Theorem pm4.71ri 560

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

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	pm4.71i 559	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 462	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anabs7  664  biadaniALT  820  orabs  1000  prlem2  1055  dfeumo  2530  dfeu  2588  2moswapv  2622  2moswap  2637  exsnrex  4640  eliunxp  5791  asymref  6077  imaindm  6260  dffun9  6529  funcnv  6569  funcnv3  6570  f1ompt  7065  eufnfv  7185  dff1o6  7232  dfom2  7824  elxp4  7878  elxp5  7879  abexex  7929  dfoprab4  8013  tpostpos  8202  brwitnlem  8448  erovlem  8763  elixp2  8851  xpsnen  9002  elom3  9577  ttrclse  9656  cardval2  9920  isinfcard  10021  infmap2  10146  elznn0nn  12519  zrevaddcl  12554  qrevaddcl  12906  hash2prb  14413  hash3tpb  14436  cotr2g  14918  climreu  15498  isprm3  16629  hashbc0  16952  imasleval  17480  xpscf  17504  isssc  17758  issubmndb  18708  isgim  19170  eldprd  19912  brric2  20391  islmim  20945  tgval2  22819  eltg2b  22822  snfil  23727  isms2  24314  setsms  24344  elii1  24807  phtpcer  24870  elovolm  25352  ellimc2  25754  limcun  25772  1cubr  26728  fsumvma2  27101  dchrelbas3  27125  2lgslem1b  27279  dmscut  27699  madeval2  27737  made0  27761  nbgrel  29243  rusgrnumwwlks  29877  isgrpo  30399  mdsl2i  32224  cvmdi  32226  rabfmpunirn  32550  zarcls  33837  eulerpartlemn  34345  bnj580  34876  bnj1049  34937  snmlval  35291  satf0suclem  35335  fmlasuc0  35344  elmthm  35536  brtxp2  35842  brpprod3a  35847  bj-elid6  37131  ismgmOLD  37817  brres2  38230  brxrn2  38330  redundpim3  38594  prtlem100  38825  islln2  39478  islpln2  39503  islvol2  39547  prjspeclsp  42573  onsucrn  43233  dflim5  43291  en2pr  43509  pren2  43515  elmapintrab  43538  clcnvlem  43585  sprvalpw  47454  sprvalpwn0  47457  prprvalpw  47489  clnbgrel  47802  eliunxp2  48295  elbigo  48513