Theorem pm4.71i 662

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)

Hypothesis

Ref	Expression
pm4.71i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
pm4.71i	⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

Proof of Theorem pm4.71i

Step	Hyp	Ref	Expression
1		pm4.71i.1	. 2 ⊢ (𝜑 → 𝜓)
2		pm4.71 660	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	mpbi 219	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm4.24  673  pm4.45  720  anabs1  846  2eu5  2545  imadmrn  5395  dff1o2  6055  f12dfv  6429  isof1oidb  6474  isof1oopb  6475  xpsnen  7929  dom0  7973  dfac5lem2  8830  pwfseqlem4  9363  axgroth6  9529  eqreznegel  11650  xrnemnf  11827  xrnepnf  11828  elioopnf  12138  elioomnf  12139  elicopnf  12140  elxrge0  12152  isprm2  15233  efgrelexlemb  17986  opsrtoslem1  19305  tgphaus  21730  cfilucfil3  22925  ioombl1lem4  23136  vitalilem1  23182  vitalilem1OLD  23183  ellogdm  24185  nb3grapr2  25983  is2wlk  26095  0spth  26101  0crct  26154  0cycl  26155  erclwwlkref  26341  erclwwlknref  26353  pjimai  28419  dfrp2  28922  eulerpartlemt0  29758  bnj1101  30109  bj-snglc  32150  icorempt2  32375  wl-cases2-dnf  32474  matunitlindf  32577  pm11.58  37612  nb3grpr2  40611  upgr2wlk  40876  erclwwlksref  41241  erclwwlksnref  41253  0spth-av  41294  0Crct  41300  0Cycl  41301