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  821  orabs  1001  prlem2  1056  dfeumo  2537  dfeu  2595  2moswapv  2629  2moswap  2644  exsnrex  4680  eliunxp  5848  asymref  6136  imaindm  6319  dffun9  6595  funcnv  6635  funcnv3  6636  f1ompt  7131  eufnfv  7249  dff1o6  7295  dfom2  7889  elxp4  7944  elxp5  7945  abexex  7996  dfoprab4  8080  tpostpos  8271  brwitnlem  8545  erovlem  8853  elixp2  8941  xpsnen  9095  elom3  9688  ttrclse  9767  cardval2  10031  isinfcard  10132  infmap2  10257  elznn0nn  12627  zrevaddcl  12662  qrevaddcl  13013  hash2prb  14511  hash3tpb  14534  cotr2g  15015  climreu  15592  isprm3  16720  hashbc0  17043  imasleval  17586  xpscf  17610  isssc  17864  issubmndb  18818  isgim  19280  eldprd  20024  brric2  20506  islmim  21061  tgval2  22963  eltg2b  22966  snfil  23872  isms2  24460  setsms  24492  elii1  24964  phtpcer  25027  elovolm  25510  ellimc2  25912  limcun  25930  1cubr  26885  fsumvma2  27258  dchrelbas3  27282  2lgslem1b  27436  dmscut  27856  madeval2  27892  made0  27912  nbgrel  29357  rusgrnumwwlks  29994  isgrpo  30516  mdsl2i  32341  cvmdi  32343  rabfmpunirn  32663  zarcls  33873  eulerpartlemn  34383  bnj580  34927  bnj1049  34988  snmlval  35336  satf0suclem  35380  fmlasuc0  35389  elmthm  35581  brtxp2  35882  brpprod3a  35887  bj-elid6  37171  ismgmOLD  37857  brres2  38269  brxrn2  38376  redundpim3  38631  prtlem100  38860  islln2  39513  islpln2  39538  islvol2  39582  prjspeclsp  42622  onsucrn  43284  dflim5  43342  en2pr  43560  pren2  43566  elmapintrab  43589  clcnvlem  43636  sprvalpw  47467  sprvalpwn0  47470  prprvalpw  47502  clnbgrel  47815  eliunxp2  48250  elbigo  48472