Theorem pm4.71ri 565

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 564	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 463	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anabs7  670  biadaniALT  826  orabs  1006  prlem2  1061  dfeumo  2540  dfeu  2599  2moswapv  2633  2moswap  2648  exsnrex  4612  eliunxp  5779  asymref  6066  imaindm  6250  dffun9  6514  funcnv  6554  funcnv3  6555  f1ompt  7052  eufnfv  7173  dff1o6  7219  dfom2  7808  elxp4  7862  elxp5  7863  abexex  7913  dfoprab4  7997  tpostpos  8186  brwitnlem  8432  erovlem  8750  elixp2  8839  xpsnen  8989  elom3  9560  ttrclse  9639  cardval2  9906  isinfcard  10005  infmap2  10130  elznn0nn  12529  zrevaddcl  12563  qrevaddcl  12912  hash2prb  14425  hash3tpb  14448  cotr2g  14929  climreu  15509  isprm3  16643  hashbc0  16967  imasleval  17496  xpscf  17520  isssc  17778  issubmndb  18764  isgim  19228  eldprd  19972  brric2  20478  islmim  21052  tgval2  22939  eltg2b  22942  snfil  23847  isms2  24433  setsms  24463  elii1  24920  phtpcer  24980  elovolm  25460  ellimc2  25862  limcun  25880  1cubr  26824  fsumvma2  27195  dchrelbas3  27219  2lgslem1b  27373  dmcuts  27801  madeval2  27843  made0  27873  nbgrel  29427  rusgrnumwwlks  30063  isgrpo  30586  mdsl2i  32411  cvmdi  32413  rabfmpunirn  32745  zarcls  34058  eulerpartlemn  34565  bnj580  35095  bnj1049  35156  snmlval  35559  satf0suclem  35603  fmlasuc0  35612  elmthm  35804  brtxp2  36107  brpprod3a  36112  bj-elid6  37530  ismgmOLD  38217  brres2  38640  ralmo  38727  brxrn2  38751  dfsuccl4  38841  redundpim3  39081  prtlem100  39351  islln2  40003  islpln2  40028  islvol2  40072  prjspeclsp  43062  onsucrn  43716  dflim5  43774  en2pr  43991  pren2  43997  elmapintrab  44020  clcnvlem  44067  sprvalpw  47955  sprvalpwn0  47958  prprvalpw  47990  clnbgrel  48319  eliunxp2  48825  elbigo  49042