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

Theorem pm4.71ri 663
 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 661 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 219 1 (𝜑 ↔ (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  biadan2  672  anabs7  848  orabs  896  prlem2  998  eu5  2484  2moswap  2535  exsnrex  4168  eliunxp  5181  asymref  5431  dffun9  5832  funcnv  5872  funcnv3  5873  f1ompt  6290  eufnfv  6395  dff1o6  6431  dfom2  6959  elxp4  7003  elxp5  7004  abexex  7042  dfoprab4  7116  tpostpos  7259  brwitnlem  7474  erovlem  7730  elixp2  7798  xpsnen  7929  elom3  8428  cardval2  8700  isinfcard  8798  infmap2  8923  elznn0nn  11268  zrevaddcl  11299  qrevaddcl  11686  hash2prb  13111  cotr2g  13563  climreu  14135  isprm3  15234  hashbc0  15547  imasleval  16024  isssc  16303  isgim  17527  eldprd  18226  brric2  18568  islmim  18883  tgval2  20571  eltg2b  20574  snfil  21478  isms2  22065  setsms  22095  elii1  22542  phtpcer  22602  phtpcerOLD  22603  elovolm  23050  ellimc2  23447  limcun  23465  1cubr  24369  fsumvma2  24739  dchrelbas3  24763  2lgslem1b  24917  rusgranumwlks  26483  isgrpo  26735  mdsl2i  28565  cvmdi  28567  rabfmpunirn  28833  eulerpartlemn  29770  bnj580  30237  bnj1049  30296  snmlval  30567  elmthm  30727  brtxp2  31158  brpprod3a  31163  ismgmOLD  32819  prtlem100  33161  islln2  33815  islpln2  33840  islvol2  33884  elmapintrab  36901  clcnvlem  36949  rusgrnumwwlks  41177  eliunxp2  41905  elbigo  42143
 Copyright terms: Public domain W3C validator