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  2530  dfeu  2588  2moswapv  2622  2moswap  2637  exsnrex  4632  eliunxp  5780  asymref  6065  imaindm  6247  dffun9  6511  funcnv  6551  funcnv3  6552  f1ompt  7045  eufnfv  7165  dff1o6  7212  dfom2  7801  elxp4  7855  elxp5  7856  abexex  7906  dfoprab4  7990  tpostpos  8179  brwitnlem  8425  erovlem  8740  elixp2  8828  xpsnen  8978  elom3  9544  ttrclse  9623  cardval2  9887  isinfcard  9986  infmap2  10111  elznn0nn  12485  zrevaddcl  12520  qrevaddcl  12872  hash2prb  14379  hash3tpb  14402  cotr2g  14883  climreu  15463  isprm3  16594  hashbc0  16917  imasleval  17445  xpscf  17469  isssc  17727  issubmndb  18679  isgim  19141  eldprd  19885  brric2  20391  islmim  20966  tgval2  22841  eltg2b  22844  snfil  23749  isms2  24336  setsms  24366  elii1  24829  phtpcer  24892  elovolm  25374  ellimc2  25776  limcun  25794  1cubr  26750  fsumvma2  27123  dchrelbas3  27147  2lgslem1b  27301  dmscut  27722  madeval2  27763  made0  27787  nbgrel  29285  rusgrnumwwlks  29919  isgrpo  30441  mdsl2i  32266  cvmdi  32268  rabfmpunirn  32596  zarcls  33841  eulerpartlemn  34349  bnj580  34880  bnj1049  34941  snmlval  35304  satf0suclem  35348  fmlasuc0  35357  elmthm  35549  brtxp2  35855  brpprod3a  35860  bj-elid6  37144  ismgmOLD  37830  brres2  38243  brxrn2  38343  redundpim3  38607  prtlem100  38838  islln2  39490  islpln2  39515  islvol2  39559  prjspeclsp  42585  onsucrn  43244  dflim5  43302  en2pr  43520  pren2  43526  elmapintrab  43549  clcnvlem  43596  sprvalpw  47464  sprvalpwn0  47467  prprvalpw  47499  clnbgrel  47812  eliunxp2  48318  elbigo  48536