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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anabs7  660  biadaniALT  817  orabs  995  prlem2  1052  dfeumo  2537  dfeu  2595  2moswapv  2631  2moswap  2646  exsnrex  4613  eliunxp  5735  asymref  6010  dffun9  6447  funcnv  6487  funcnv3  6488  f1ompt  6967  eufnfv  7087  dff1o6  7128  dfom2  7689  elxp4  7743  elxp5  7744  abexex  7787  dfoprab4  7868  tpostpos  8033  brwitnlem  8299  erovlem  8560  elixp2  8647  xpsnen  8796  elom3  9336  cardval2  9680  isinfcard  9779  infmap2  9905  elznn0nn  12263  zrevaddcl  12295  qrevaddcl  12640  hash2prb  14114  cotr2g  14615  climreu  15193  isprm3  16316  hashbc0  16634  imasleval  17169  xpscf  17193  isssc  17449  issubmndb  18359  isgim  18793  eldprd  19522  brric2  19904  islmim  20239  tgval2  22014  eltg2b  22017  snfil  22923  isms2  23511  setsms  23541  elii1  24004  phtpcer  24064  elovolm  24544  ellimc2  24946  limcun  24964  1cubr  25897  fsumvma2  26267  dchrelbas3  26291  2lgslem1b  26445  nbgrel  27610  rusgrnumwwlks  28240  isgrpo  28760  mdsl2i  30585  cvmdi  30587  rabfmpunirn  30892  zarcls  31726  eulerpartlemn  32248  bnj580  32793  bnj1049  32854  snmlval  33193  satf0suclem  33237  fmlasuc0  33246  elmthm  33438  imaindm  33659  ttrclse  33713  dmscut  33932  madeval2  33964  made0  33984  brtxp2  34110  brpprod3a  34115  bj-elid6  35268  ismgmOLD  35935  brres2  36334  brxrn2  36432  redundpim3  36670  prtlem100  36800  islln2  37452  islpln2  37477  islvol2  37521  prjspeclsp  40372  en2pr  41043  pren2  41049  elmapintrab  41073  clcnvlem  41120  sprvalpw  44820  sprvalpwn0  44823  prprvalpw  44855  eliunxp2  45557  elbigo  45785