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  2536  dfeu  2594  2moswapv  2628  2moswap  2643  exsnrex  4656  eliunxp  5817  asymref  6105  imaindm  6288  dffun9  6565  funcnv  6605  funcnv3  6606  f1ompt  7101  eufnfv  7221  dff1o6  7268  dfom2  7863  elxp4  7918  elxp5  7919  abexex  7970  dfoprab4  8054  tpostpos  8245  brwitnlem  8519  erovlem  8827  elixp2  8915  xpsnen  9069  elom3  9662  ttrclse  9741  cardval2  10005  isinfcard  10106  infmap2  10231  elznn0nn  12602  zrevaddcl  12637  qrevaddcl  12987  hash2prb  14490  hash3tpb  14513  cotr2g  14995  climreu  15572  isprm3  16702  hashbc0  17025  imasleval  17555  xpscf  17579  isssc  17833  issubmndb  18783  isgim  19245  eldprd  19987  brric2  20466  islmim  21020  tgval2  22894  eltg2b  22897  snfil  23802  isms2  24389  setsms  24419  elii1  24882  phtpcer  24945  elovolm  25428  ellimc2  25830  limcun  25848  1cubr  26804  fsumvma2  27177  dchrelbas3  27201  2lgslem1b  27355  dmscut  27775  madeval2  27813  made0  27837  nbgrel  29319  rusgrnumwwlks  29956  isgrpo  30478  mdsl2i  32303  cvmdi  32305  rabfmpunirn  32631  zarcls  33905  eulerpartlemn  34413  bnj580  34944  bnj1049  35005  snmlval  35353  satf0suclem  35397  fmlasuc0  35406  elmthm  35598  brtxp2  35899  brpprod3a  35904  bj-elid6  37188  ismgmOLD  37874  brres2  38286  brxrn2  38393  redundpim3  38648  prtlem100  38877  islln2  39530  islpln2  39555  islvol2  39599  prjspeclsp  42635  onsucrn  43295  dflim5  43353  en2pr  43571  pren2  43577  elmapintrab  43600  clcnvlem  43647  sprvalpw  47494  sprvalpwn0  47497  prprvalpw  47529  clnbgrel  47842  eliunxp2  48309  elbigo  48531