Theorem pm4.71ri 569

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 568	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 467	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anabs7  676  biadaniALT  832  orabs  1014  prlem2  1069  dfeumo  2566  dfeu  2625  2moswapv  2659  2moswap  2674  exsnrex  4642  eliunxp  5814  asymref  6107  imaindm  6290  dffun9  6554  funcnv  6594  funcnv3  6595  f1ompt  7096  eufnfv  7217  dff1o6  7263  dfom2  7852  elxp4  7907  elxp5  7908  abexex  7956  dfoprab4  8040  tpostpos  8230  brwitnlem  8480  erovlem  8799  elixp2  8887  xpsnen  9037  elom3  9605  ttrclse  9684  cardval2  9965  isinfcard  10064  infmap2  10188  elznn0nn  12596  zrevaddcl  12630  qrevaddcl  12986  hash2prb  14499  hash3tpb  14522  cotr2g  15003  climreu  15597  isprm3  16731  hashbc0  17055  imasleval  17585  xpscf  17609  isssc  17867  issubmndb  18853  isgim  19323  eldprd  20067  brric2  20580  islmim  21152  tgval2  23074  eltg2b  23077  snfil  23982  isms2  24568  setsms  24598  elii1  25055  phtpcer  25115  elovolm  25595  ellimc2  25997  limcun  26015  1cubr  26965  fsumvma2  27336  dchrelbas3  27360  2lgslem1b  27514  dmcuts  27942  madeval2  27984  made0  28014  nbgrel  29599  rusgrnumwwlks  30235  isgrpo  30758  mdsl2i  32583  cvmdi  32585  rabfmpunirn  32910  zarcls  34181  eulerpartlemn  34688  bnj580  35218  bnj1049  35279  snmlval  35694  satf0suclem  35738  fmlasuc0  35747  elmthm  35939  brtxp2  36242  brpprod3a  36247  bj-elid6  37674  ismgmOLD  38361  brres2  38784  ralmo  38871  brxrn2  38895  dfsuccl4  38985  redundpim3  39225  prtlem100  39495  islln2  40147  islpln2  40172  islvol2  40216  prjspeclsp  43206  onsucrn  43860  dflim5  43918  en2pr  44135  pren2  44141  elmapintrab  44164  clcnvlem  44211  sprvalpw  48084  sprvalpwn0  48087  prprvalpw  48119  clnbgrel  48448  eliunxp2  48965  elbigo  49182