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 552
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 550 . 2 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜓𝜑)))
31, 2mpbi 221 1 (𝜑 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  anabs7  646  biadan2  844  orabs  1012  prlem2  1071  eu5  2658  2moswap  2711  exsnrex  4414  eliunxp  5461  asymref  5723  dffun9  6130  funcnv  6169  funcnv3  6170  f1ompt  6603  eufnfv  6716  dff1o6  6755  dfom2  7297  elxp4  7340  elxp5  7341  abexex  7381  dfoprab4  7457  tpostpos  7607  brwitnlem  7824  erovlem  8079  elixp2  8149  xpsnen  8283  elom3  8792  cardval2  9100  isinfcard  9198  infmap2  9325  elznn0nn  11657  zrevaddcl  11688  qrevaddcl  12029  hash2prb  13471  cotr2g  13940  climreu  14510  isprm3  15614  hashbc0  15926  imasleval  16406  isssc  16684  isgim  17906  eldprd  18605  brric2  18949  islmim  19269  tgval2  20974  eltg2b  20977  snfil  21881  isms2  22468  setsms  22498  elii1  22947  phtpcer  23007  elovolm  23456  ellimc2  23855  limcun  23873  1cubr  24783  fsumvma2  25153  dchrelbas3  25177  2lgslem1b  25331  nbgrel  26449  rusgrnumwwlks  27116  isgrpo  27680  mdsl2i  29509  cvmdi  29511  rabfmpunirn  29780  eulerpartlemn  30768  bnj580  31306  bnj1049  31365  snmlval  31636  elmthm  31796  imaindm  32002  dmscut  32239  madeval2  32257  brtxp2  32309  brpprod3a  32314  ismgmOLD  33960  brres2  34352  brxrn2  34450  prtlem100  34638  islln2  35291  islpln2  35316  islvol2  35360  elmapintrab  38382  clcnvlem  38430  sprvalpw  42298  sprvalpwn0  42301  eliunxp2  42680  elbigo  42913
  Copyright terms: Public domain W3C validator