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  2603  2eu5  2685  dfid2  5560  imadmrn  6074  dff1o2  6830  f12dfv  7280  isof1oidb  7331  isof1oopb  7332  xpsnen  9056  dfac5lem2  10124  axgroth6  10828  eqreznegel  12974  xrnemnf  13158  xrnepnf  13159  dfrp2  13437  elioopnf  13486  elioomnf  13487  elicopnf  13488  elxrge0  13500  isprm2  16762  efgrelexlemb  19864  opsrtoslem1  22256  tgphaus  24325  cfilucfil3  25530  ioombl1lem4  25771  vitalilem1  25818  ellogdm  26855  nb3grpr2  29791  upgr2wlk  30074  erclwwlkref  30438  erclwwlknref  30487  0spth  30544  0crct  30551  pjimai  32599  eulerpartlemt0  34824  bnj1101  35238  satfvsuclem2  35889  bj-snglc  37662  bj-epelb  37762  bj-opelidb1  37854  icorempo  38054  wl-cases2-dnf  38224  matunitlindf  38326  disjressuc2  39118  dflim5  44114  pm11.58  45158