Theorem pm4.71ri 570

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabs7  677  biadaniALT  833  orabs  1014  prlem2  1071  dfeumo  2566  dfeu  2625  2moswapv  2659  2moswap  2674  exsnrex  4648  eliunxp  5825  asymref  6118  imaindm  6304  dffun9  6569  funcnv  6609  funcnv3  6610  f1ompt  7110  eufnfv  7234  dff1o6  7282  dfom2  7870  elxp4  7925  elxp5  7926  abexex  7974  dfoprab4  8058  tpostpos  8248  brwitnlem  8498  erovlem  8817  elixp2  8905  xpsnen  9056  elom3  9624  ttrclse  9703  cardval2  9993  isinfcard  10092  infmap2  10216  elznn0nn  12622  zrevaddcl  12656  qrevaddcl  13013  hash2prb  14529  hash3tpb  14552  cotr2g  15039  climreu  15633  isprm3  16765  hashbc0  17089  imasleval  17619  xpscf  17643  isssc  17901  issubmndb  18902  isgim  19378  eldprd  20122  isbrric2  20653  islmim  21235  tgval2  23165  eltg2b  23168  snfil  24074  isms2  24660  setsms  24690  elii1  25147  phtpcer  25207  elovolm  25687  ellimc2  26089  limcun  26107  1cubr  27060  fsumvma2  27431  dchrelbas3  27455  2lgslem1b  27609  dmcuts  28037  madeval2  28079  made0  28109  nbgrel  29750  rusgrnumwwlks  30395  isgrpo  30922  mdsl2i  32747  cvmdi  32749  rabfmpunirn  33071  zarcls  34330  eulerpartlemn  34838  bnj580  35368  bnj1049  35429  snmlval  35862  satf0suclem  35906  fmlasuc0  35915  elmthm  36107  brtxp2  36410  brpprod3a  36415  bj-elid6  37873  ismgmOLD  38561  brres2  38982  ralmo  39069  brxrn2  39093  dfsuccl4  39183  redundpim3  39423  prtlem100  39693  islln2  40345  islpln2  40370  islvol2  40414  prjspeclsp  43404  onsucrn  44058  dflim5  44116  en2pr  44333  pren2  44339  elmapintrab  44362  clcnvlem  44409  sprvalpw  48289  sprvalpwn0  48292  prprvalpw  48324  clnbgrel  48653  eliunxp2  49173  elbigo  49390