Theorem pm4.71i 665

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 663	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	mpbi 220	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  pm4.24  676  pm4.45  724  anabs1  867  2eu5  2586  rabeqc  3394  imadmrn  5511  dff1o2  6180  f12dfv  6569  isof1oidb  6614  isof1oopb  6615  xpsnen  8085  dom0  8129  dfac5lem2  8985  pwfseqlem4  9522  axgroth6  9688  eqreznegel  11812  xrnemnf  11989  xrnepnf  11990  elioopnf  12305  elioomnf  12306  elicopnf  12307  elxrge0  12319  isprm2  15442  efgrelexlemb  18209  opsrtoslem1  19532  tgphaus  21967  cfilucfil3  23163  ioombl1lem4  23375  vitalilem1  23422  ellogdm  24430  nb3grpr2  26329  upgr2wlk  26620  erclwwlkref  26977  erclwwlknref  27033  0spth  27104  0crct  27111  pjimai  29163  dfrp2  29660  eulerpartlemt0  30559  bnj1101  30981  bj-snglc  33082  icorempt2  33329  wl-cases2-dnf  33425  matunitlindf  33537  pm11.58  38907