MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71ri Structured version   Visualization version   GIF version

Theorem pm4.71ri 668
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
Hypothesis
Ref Expression
pm4.71ri.1 (𝜑𝜓)
Assertion
Ref Expression
pm4.71ri (𝜑 ↔ (𝜓𝜑))

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . 2 (𝜑𝜓)
2 pm4.71r 666 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 220 1 (𝜑 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  biadan2  677  anabs7  887  orabs  936  prlem2  1044  eu5  2629  2moswap  2681  exsnrex  4361  eliunxp  5411  asymref  5666  dffun9  6074  funcnv  6115  funcnv3  6116  f1ompt  6541  eufnfv  6650  dff1o6  6690  dfom2  7228  elxp4  7271  elxp5  7272  abexex  7312  dfoprab4  7388  tpostpos  7537  brwitnlem  7752  erovlem  8006  elixp2  8074  xpsnen  8205  elom3  8714  cardval2  9003  isinfcard  9101  infmap2  9228  elznn0nn  11579  zrevaddcl  11610  qrevaddcl  11999  hash2prb  13442  cotr2g  13912  climreu  14482  isprm3  15594  hashbc0  15907  imasleval  16399  isssc  16677  isgim  17901  eldprd  18599  brric2  18943  islmim  19260  tgval2  20958  eltg2b  20961  snfil  21865  isms2  22452  setsms  22482  elii1  22931  phtpcer  22991  elovolm  23439  ellimc2  23836  limcun  23854  1cubr  24764  fsumvma2  25134  dchrelbas3  25158  2lgslem1b  25312  nbgrel  26428  rusgrnumwwlks  27092  isgrpo  27656  mdsl2i  29486  cvmdi  29488  rabfmpunirn  29758  eulerpartlemn  30748  bnj580  31286  bnj1049  31345  snmlval  31616  elmthm  31776  imaindm  31983  dmscut  32220  madeval2  32238  brtxp2  32290  brpprod3a  32295  ismgmOLD  33958  brres2  34355  brxrn2  34456  prtlem100  34644  islln2  35296  islpln2  35321  islvol2  35365  elmapintrab  38380  clcnvlem  38428  sprvalpw  42236  sprvalpwn0  42239  eliunxp2  42618  elbigo  42851
  Copyright terms: Public domain W3C validator