Theorem pm4.71i 561

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  pm4.71ri  562  pm4.24  565  anabs1  661  pm4.45im  827  pm4.45  997  eu6lem  2568  2eu5  2652  rabeqcOLD  3680  dfid2  5575  imadmrn  6067  dff1o2  6835  f12dfv  7266  isof1oidb  7316  isof1oopb  7317  xpsnen  9051  dom0OLD  9099  dfac5lem2  10115  pwfseqlem4  10653  axgroth6  10819  eqreznegel  12914  xrnemnf  13093  xrnepnf  13094  dfrp2  13369  elioopnf  13416  elioomnf  13417  elicopnf  13418  elxrge0  13430  isprm2  16615  efgrelexlemb  19611  opsrtoslem1  21598  tgphaus  23603  cfilucfil3  24819  ioombl1lem4  25060  vitalilem1  25107  ellogdm  26129  nb3grpr2  28620  upgr2wlk  28905  erclwwlkref  29253  erclwwlknref  29302  0spth  29359  0crct  29366  pjimai  31407  eulerpartlemt0  33306  bnj1101  33733  satfvsuclem2  34289  bj-snglc  35788  bj-epelb  35888  bj-opelidb1  35972  icorempo  36170  wl-cases2-dnf  36319  matunitlindf  36424  disjressuc2  37196  dflim5  42012  pm11.58  43082