Theorem pm4.71i 563

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  pm4.71ri  564  pm4.24  567  anabs1  662  pm4.45im  827  pm4.45  997  eu6lem  2575  2eu5  2659  rabeqc  3591  imadmrn  5923  dff1o2  6635  f12dfv  7053  isof1oidb  7102  isof1oopb  7103  xpsnen  8662  dom0  8707  dfac5lem2  9636  pwfseqlem4  10174  axgroth6  10340  eqreznegel  12428  xrnemnf  12607  xrnepnf  12608  dfrp2  12882  elioopnf  12929  elioomnf  12930  elicopnf  12931  elxrge0  12943  isprm2  16135  efgrelexlemb  19006  opsrtoslem1  20878  tgphaus  22880  cfilucfil3  24084  ioombl1lem4  24325  vitalilem1  24372  ellogdm  25394  nb3grpr2  27337  upgr2wlk  27622  erclwwlkref  27969  erclwwlknref  28018  0spth  28075  0crct  28082  pjimai  30123  eulerpartlemt0  31918  bnj1101  32347  satfvsuclem2  32905  bj-snglc  34814  bj-epelb  34894  bj-opelidb1  34977  icorempo  35177  wl-cases2-dnf  35326  matunitlindf  35430  pm11.58  41586