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  2595  2moswapv  2629  2moswap  2644  exsnrex  4637  eliunxp  5786  asymref  6073  imaindm  6257  dffun9  6521  funcnv  6561  funcnv3  6562  f1ompt  7056  eufnfv  7175  dff1o6  7221  dfom2  7810  elxp4  7864  elxp5  7865  abexex  7915  dfoprab4  7999  tpostpos  8188  brwitnlem  8434  erovlem  8750  elixp2  8839  xpsnen  8989  elom3  9557  ttrclse  9636  cardval2  9903  isinfcard  10002  infmap2  10127  elznn0nn  12502  zrevaddcl  12536  qrevaddcl  12884  hash2prb  14395  hash3tpb  14418  cotr2g  14899  climreu  15479  isprm3  16610  hashbc0  16933  imasleval  17462  xpscf  17486  isssc  17744  issubmndb  18730  isgim  19191  eldprd  19935  brric2  20439  islmim  21014  tgval2  22900  eltg2b  22903  snfil  23808  isms2  24394  setsms  24424  elii1  24887  phtpcer  24950  elovolm  25432  ellimc2  25834  limcun  25852  1cubr  26808  fsumvma2  27181  dchrelbas3  27205  2lgslem1b  27359  dmcuts  27787  madeval2  27829  made0  27859  nbgrel  29413  rusgrnumwwlks  30050  isgrpo  30572  mdsl2i  32397  cvmdi  32399  rabfmpunirn  32731  zarcls  34031  eulerpartlemn  34538  bnj580  35069  bnj1049  35130  snmlval  35525  satf0suclem  35569  fmlasuc0  35578  elmthm  35770  brtxp2  36073  brpprod3a  36078  bj-elid6  37375  ismgmOLD  38051  brres2  38466  brxrn2  38569  dfsuccl4  38648  redundpim3  38887  prtlem100  39119  islln2  39771  islpln2  39796  islvol2  39840  prjspeclsp  42855  onsucrn  43513  dflim5  43571  en2pr  43788  pren2  43794  elmapintrab  43817  clcnvlem  43864  sprvalpw  47726  sprvalpwn0  47729  prprvalpw  47761  clnbgrel  48074  eliunxp2  48580  elbigo  48797