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  2564  dfeu  2623  2moswapv  2657  2moswap  2672  exsnrex  4642  eliunxp  5824  asymref  6128  imaindm  6328  dffun9  6597  funcnv  6639  funcnv3  6640  f1ompt  7143  eufnfv  7266  dff1o6  7314  dfom2  7913  elxp4  7968  elxp5  7969  abexex  8017  dfoprab4  8101  tpostpos  8301  brwitnlem  8553  erovlem  8872  elixp2  8967  xpsnen  9118  elom3  9686  ttrclse  9765  cardval2  10111  isinfcard  10210  infmap2  10334  elznn0nn  12747  zrevaddcl  12781  qrevaddcl  13139  hash2prb  14658  hash3tpb  14681  cotr2g  15172  climreu  15767  isprm3  16902  hashbc0  17227  imasleval  17763  xpscf  17787  isssc  18045  issubmndb  19050  isgim  19526  eldprd  20271  isbrric2  20804  islmim  21388  tgval2  23329  eltg2b  23332  snfil  24238  isms2  24824  setsms  24854  elii1  25311  phtpcer  25371  elovolm  25851  ellimc2  26252  limcun  26270  1cubr  27227  fsumvma2  27598  dchrelbas3  27622  2lgslem1b  27776  dmcuts  28234  madeval2  28276  made0  28306  nbgrel  29978  rusgrnumwwlks  30623  isgrpo  31156  mdsl2i  32981  cvmdi  32983  rabfmpunirn  33345  zarcls  34617  eulerpartlemn  35124  bnj580  35654  bnj1049  35715  fwfffunres  35829  dmr0ss  36043  dfk12  36053  dfk22  36054  dfk32  36055  snmlval  36304  satf0suclem  36348  fmlasuc0  36357  elmthm  36549  brtxp2  36858  brpprod3a  36863  bj-inxpALT  38176  bj-elid6  38359  ismgmOLD  39050  brres2  39471  ralmo  39558  brxrn2  39582  dfsuccl4  39672  redundpim3  39912  prtlem100  40182  islln2  40834  islpln2  40859  islvol2  40903  prjspeclsp  43906  onsucrn  44534  dflim5  44592  en2pr  44809  pren2  44815  elmapintrab  44838  clcnvlem  44884  sprvalpw  48835  sprvalpwn0  48838  prprvalpw  48870  clnbgrel  49199  eliunxp2  49777  elbigo  49994  rrx2xpref1o  50162