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  1071  dfeumo  2564  dfeu  2623  2moswapv  2657  2moswap  2672  exsnrex  4646  eliunxp  5823  asymref  6116  imaindm  6300  dffun9  6565  funcnv  6605  funcnv3  6606  f1ompt  7106  eufnfv  7227  dff1o6  7273  dfom2  7860  elxp4  7915  elxp5  7916  abexex  7964  dfoprab4  8048  tpostpos  8238  brwitnlem  8488  erovlem  8807  elixp2  8895  xpsnen  9045  elom3  9613  ttrclse  9692  cardval2  9973  isinfcard  10072  infmap2  10196  elznn0nn  12600  zrevaddcl  12634  qrevaddcl  12990  hash2prb  14505  hash3tpb  14528  cotr2g  15009  climreu  15603  isprm3  16736  hashbc0  17060  imasleval  17590  xpscf  17614  isssc  17872  issubmndb  18858  isgim  19327  eldprd  20071  isbrric2  20601  islmim  21183  tgval2  23113  eltg2b  23116  snfil  24021  isms2  24607  setsms  24637  elii1  25094  phtpcer  25154  elovolm  25634  ellimc2  26036  limcun  26054  1cubr  27007  fsumvma2  27378  dchrelbas3  27402  2lgslem1b  27556  dmcuts  27984  madeval2  28026  made0  28056  nbgrel  29690  rusgrnumwwlks  30326  isgrpo  30849  mdsl2i  32674  cvmdi  32676  rabfmpunirn  32998  zarcls  34264  eulerpartlemn  34771  bnj580  35301  bnj1049  35362  snmlval  35823  satf0suclem  35867  fmlasuc0  35876  elmthm  36068  brtxp2  36371  brpprod3a  36376  bj-elid6  37814  ismgmOLD  38501  brres2  38922  ralmo  39009  brxrn2  39033  dfsuccl4  39123  redundpim3  39363  prtlem100  39633  islln2  40285  islpln2  40310  islvol2  40354  prjspeclsp  43344  onsucrn  43998  dflim5  44056  en2pr  44273  pren2  44279  elmapintrab  44302  clcnvlem  44349  sprvalpw  48229  sprvalpwn0  48232  prprvalpw  48264  clnbgrel  48593  eliunxp2  49114  elbigo  49331