Theorem pm4.71i 569

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm4.71ri  570  pm4.24  574  anabs1  675  pm4.45im  841  pm4.45  1013  eu6lem  2598  2eu5  2680  dfid2  5548  imadmrnOLD  6070  dff1o2  6835  f12dfv  7285  isof1oidb  7336  isof1oopb  7337  xpsnen  9087  dfac5lem2  10210  axgroth6  10920  eqreznegel  13068  xrnemnf  13253  xrnepnf  13254  dfrp2  13532  elioopnf  13581  elioomnf  13582  elicopnf  13583  elxrge0  13595  isprm2  16866  efgrelexlemb  19973  opsrtoslem1  22373  matunitlindf  23005  tgphaus  24445  cfilucfil3  25650  ioombl1lem4  25891  vitalilem1  25938  ellogdm  26976  nb3grpr2  29973  upgr2wlk  30256  erclwwlkref  30620  erclwwlknref  30669  0spth  30726  0crct  30733  pjimai  32787  eulerpartlemt0  35051  bnj1101  35465  satfvsuclem2  36215  bj-snglc  37978  bj-epelb  38092  bj-opelidb1  38183  icorempo  38383  wl-cases2-dnf  38553  disjressuc2  39452  dflim5  44440  pm11.58  45483