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  2599  2eu5  2681  dfid2  5548  imadmrnOLD  6068  dff1o2  6828  f12dfv  7279  isof1oidb  7330  isof1oopb  7331  xpsnen  9073  dfac5lem2  10196  axgroth6  10906  eqreznegel  13054  xrnemnf  13239  xrnepnf  13240  dfrp2  13518  elioopnf  13567  elioomnf  13568  elicopnf  13569  elxrge0  13581  isprm2  16850  efgrelexlemb  19957  opsrtoslem1  22357  matunitlindf  22989  tgphaus  24429  cfilucfil3  25634  ioombl1lem4  25875  vitalilem1  25922  ellogdm  26960  nb3grpr2  29957  upgr2wlk  30240  erclwwlkref  30604  erclwwlknref  30653  0spth  30710  0crct  30717  pjimai  32771  eulerpartlemt0  34994  bnj1101  35408  satfvsuclem2  36104  bj-snglc  37862  bj-epelb  37964  bj-opelidb1  38054  icorempo  38254  wl-cases2-dnf  38424  disjressuc2  39323  dflim5  44315  pm11.58  45359