Theorem pm4.71ri 561

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anabs7  661  biadaniALT  818  orabs  996  prlem2  1053  dfeumo  2537  dfeu  2595  2moswapv  2631  2moswap  2646  exsnrex  4616  eliunxp  5746  asymref  6021  dffun9  6463  funcnv  6503  funcnv3  6504  f1ompt  6985  eufnfv  7105  dff1o6  7147  dfom2  7714  elxp4  7769  elxp5  7770  abexex  7814  dfoprab4  7895  tpostpos  8062  brwitnlem  8337  erovlem  8602  elixp2  8689  xpsnen  8842  elom3  9406  ttrclse  9485  cardval2  9749  isinfcard  9848  infmap2  9974  elznn0nn  12333  zrevaddcl  12365  qrevaddcl  12711  hash2prb  14186  cotr2g  14687  climreu  15265  isprm3  16388  hashbc0  16706  imasleval  17252  xpscf  17276  isssc  17532  issubmndb  18444  isgim  18878  eldprd  19607  brric2  19989  islmim  20324  tgval2  22106  eltg2b  22109  snfil  23015  isms2  23603  setsms  23635  elii1  24098  phtpcer  24158  elovolm  24639  ellimc2  25041  limcun  25059  1cubr  25992  fsumvma2  26362  dchrelbas3  26386  2lgslem1b  26540  nbgrel  27707  rusgrnumwwlks  28339  isgrpo  28859  mdsl2i  30684  cvmdi  30686  rabfmpunirn  30990  zarcls  31824  eulerpartlemn  32348  bnj580  32893  bnj1049  32954  snmlval  33293  satf0suclem  33337  fmlasuc0  33346  elmthm  33538  imaindm  33753  dmscut  34005  madeval2  34037  made0  34057  brtxp2  34183  brpprod3a  34188  bj-elid6  35341  ismgmOLD  36008  brres2  36407  brxrn2  36505  redundpim3  36743  prtlem100  36873  islln2  37525  islpln2  37550  islvol2  37594  prjspeclsp  40451  en2pr  41154  pren2  41160  elmapintrab  41184  clcnvlem  41231  sprvalpw  44932  sprvalpwn0  44935  prprvalpw  44967  eliunxp2  45669  elbigo  45897