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  5552  imadmrn  6066  dff1o2  6823  f12dfv  7274  isof1oidb  7325  isof1oopb  7326  xpsnen  9059  dfac5lem2  10127  axgroth6  10837  eqreznegel  12983  xrnemnf  13168  xrnepnf  13169  dfrp2  13447  elioopnf  13496  elioomnf  13497  elicopnf  13498  elxrge0  13510  isprm2  16772  efgrelexlemb  19877  opsrtoslem1  22271  matunitlindf  22903  tgphaus  24343  cfilucfil3  25548  ioombl1lem4  25789  vitalilem1  25836  ellogdm  26876  nb3grpr2  29843  upgr2wlk  30126  erclwwlkref  30490  erclwwlknref  30539  0spth  30596  0crct  30603  pjimai  32657  eulerpartlemt0  34880  bnj1101  35294  satfvsuclem2  35939  bj-snglc  37713  bj-epelb  37813  bj-opelidb1  37905  icorempo  38105  wl-cases2-dnf  38275  disjressuc2  39159  dflim5  44170  pm11.58  45214