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  2561  dfeu  2620  2moswapv  2654  2moswap  2669  exsnrex  4641  eliunxp  5817  asymref  6110  imaindm  6297  dffun9  6563  funcnv  6603  funcnv3  6604  f1ompt  7105  eufnfv  7229  dff1o6  7277  dfom2  7865  elxp4  7920  elxp5  7921  abexex  7969  dfoprab4  8053  tpostpos  8245  brwitnlem  8495  erovlem  8814  elixp2  8909  xpsnen  9060  elom3  9628  ttrclse  9707  cardval2  9997  isinfcard  10096  infmap2  10220  elznn0nn  12630  zrevaddcl  12664  qrevaddcl  13022  hash2prb  14538  hash3tpb  14561  cotr2g  15050  climreu  15644  isprm3  16774  hashbc0  17098  imasleval  17628  xpscf  17652  isssc  17910  issubmndb  18914  isgim  19390  eldprd  20134  isbrric2  20665  islmim  21247  tgval2  23182  eltg2b  23185  snfil  24091  isms2  24677  setsms  24707  elii1  25164  phtpcer  25224  elovolm  25704  ellimc2  26105  limcun  26123  1cubr  27080  fsumvma2  27451  dchrelbas3  27475  2lgslem1b  27629  dmcuts  28057  madeval2  28099  made0  28129  nbgrel  29801  rusgrnumwwlks  30446  isgrpo  30979  mdsl2i  32804  cvmdi  32806  rabfmpunirn  33127  zarcls  34385  eulerpartlemn  34893  bnj580  35423  bnj1049  35484  snmlval  35911  satf0suclem  35955  fmlasuc0  35964  elmthm  36156  brtxp2  36459  brpprod3a  36464  bj-elid6  37923  ismgmOLD  38601  brres2  39022  ralmo  39109  brxrn2  39133  dfsuccl4  39223  redundpim3  39463  prtlem100  39733  islln2  40385  islpln2  40410  islvol2  40454  prjspeclsp  43459  onsucrn  44113  dflim5  44171  en2pr  44388  pren2  44394  elmapintrab  44417  clcnvlem  44464  sprvalpw  48381  sprvalpwn0  48384  prprvalpw  48416  clnbgrel  48745  eliunxp2  49265  elbigo  49482