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  1000  prlem2  1055  dfeumo  2535  dfeu  2593  2moswapv  2627  2moswap  2642  exsnrex  4685  eliunxp  5851  asymref  6139  imaindm  6321  dffun9  6597  funcnv  6637  funcnv3  6638  f1ompt  7131  eufnfv  7249  dff1o6  7295  dfom2  7889  elxp4  7945  elxp5  7946  abexex  7995  dfoprab4  8079  tpostpos  8270  brwitnlem  8544  erovlem  8852  elixp2  8940  xpsnen  9094  elom3  9686  ttrclse  9765  cardval2  10029  isinfcard  10130  infmap2  10255  elznn0nn  12625  zrevaddcl  12660  qrevaddcl  13011  hash2prb  14508  hash3tpb  14531  cotr2g  15012  climreu  15589  isprm3  16717  hashbc0  17039  imasleval  17588  xpscf  17612  isssc  17868  issubmndb  18831  isgim  19293  eldprd  20039  brric2  20523  islmim  21079  tgval2  22979  eltg2b  22982  snfil  23888  isms2  24476  setsms  24508  elii1  24978  phtpcer  25041  elovolm  25524  ellimc2  25927  limcun  25945  1cubr  26900  fsumvma2  27273  dchrelbas3  27297  2lgslem1b  27451  dmscut  27871  madeval2  27907  made0  27927  nbgrel  29372  rusgrnumwwlks  30004  isgrpo  30526  mdsl2i  32351  cvmdi  32353  rabfmpunirn  32670  zarcls  33835  eulerpartlemn  34363  bnj580  34906  bnj1049  34967  snmlval  35316  satf0suclem  35360  fmlasuc0  35369  elmthm  35561  brtxp2  35863  brpprod3a  35868  bj-elid6  37153  ismgmOLD  37837  brres2  38250  brxrn2  38357  redundpim3  38612  prtlem100  38841  islln2  39494  islpln2  39519  islvol2  39563  prjspeclsp  42599  onsucrn  43261  dflim5  43319  en2pr  43537  pren2  43543  elmapintrab  43566  clcnvlem  43613  sprvalpw  47405  sprvalpwn0  47408  prprvalpw  47440  clnbgrel  47753  eliunxp2  48179  elbigo  48401