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  2561  dfeu  2620  2moswapv  2654  2moswap  2669  exsnrex  4637  eliunxp  5815  asymref  6112  imaindm  6305  dffun9  6574  funcnv  6614  funcnv3  6615  f1ompt  7116  eufnfv  7239  dff1o6  7287  dfom2  7883  elxp4  7938  elxp5  7939  abexex  7987  dfoprab4  8071  tpostpos  8271  brwitnlem  8523  erovlem  8842  elixp2  8937  xpsnen  9088  elom3  9656  ttrclse  9735  cardval2  10079  isinfcard  10178  infmap2  10302  elznn0nn  12714  zrevaddcl  12748  qrevaddcl  13106  hash2prb  14624  hash3tpb  14647  cotr2g  15138  climreu  15732  isprm3  16867  hashbc0  17192  imasleval  17722  xpscf  17746  isssc  18004  issubmndb  19009  isgim  19485  eldprd  20229  isbrric2  20762  islmim  21346  tgval2  23283  eltg2b  23286  snfil  24192  isms2  24778  setsms  24808  elii1  25265  phtpcer  25325  elovolm  25805  ellimc2  26206  limcun  26224  1cubr  27179  fsumvma2  27550  dchrelbas3  27574  2lgslem1b  27728  dmcuts  28186  madeval2  28228  made0  28258  nbgrel  29930  rusgrnumwwlks  30575  isgrpo  31108  mdsl2i  32933  cvmdi  32935  rabfmpunirn  33298  zarcls  34556  eulerpartlemn  35063  bnj580  35593  bnj1049  35654  fwfffunres  35768  dmr0ss  35953  dfk12  35963  dfk22  35964  dfk32  35965  snmlval  36214  satf0suclem  36258  fmlasuc0  36267  elmthm  36459  brtxp2  36767  brpprod3a  36772  bj-elid6  38228  ismgmOLD  38921  brres2  39342  ralmo  39429  brxrn2  39453  dfsuccl4  39543  redundpim3  39783  prtlem100  40053  islln2  40705  islpln2  40730  islvol2  40774  prjspeclsp  43777  onsucrn  44410  dflim5  44468  en2pr  44685  pren2  44691  elmapintrab  44714  clcnvlem  44760  sprvalpw  48698  sprvalpwn0  48701  prprvalpw  48733  clnbgrel  49062  eliunxp2  49582  elbigo  49799  rrx2xpref1o  49967