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  2601  2eu5  2683  dfid2  5555  imadmrnOLD  6086  dff1o2  6860  f12dfv  7312  isof1oidb  7363  isof1oopb  7364  xpsnen  9118  dfac5lem2  10242  axgroth6  10952  eqreznegel  13101  xrnemnf  13286  xrnepnf  13287  dfrp2  13565  elioopnf  13614  elioomnf  13615  elicopnf  13616  elxrge0  13628  isprm2  16901  efgrelexlemb  20015  opsrtoslem1  22419  matunitlindf  23051  tgphaus  24491  cfilucfil3  25696  ioombl1lem4  25937  vitalilem1  25984  ellogdm  27024  nb3grpr2  30021  upgr2wlk  30304  erclwwlkref  30668  erclwwlknref  30717  0spth  30774  0crct  30781  pjimai  32835  eulerpartlemt0  35112  bnj1101  35526  satfvsuclem2  36333  bj-snglc  38097  bj-epelb  38254  bj-opelidb1  38342  icorempo  38542  wl-cases2-dnf  38712  disjressuc2  39609  dflim5  44592  pm11.58  45635