Theorem pm4.71i 559

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm4.71ri  560  pm4.24  563  anabs1  663  pm4.45im  828  pm4.45  1000  eu6lem  2574  2eu5  2657  dfid2  5529  imadmrn  6037  dff1o2  6787  f12dfv  7229  isof1oidb  7280  isof1oopb  7281  xpsnen  9001  dfac5lem2  10046  axgroth6  10751  eqreznegel  12859  xrnemnf  13043  xrnepnf  13044  dfrp2  13322  elioopnf  13371  elioomnf  13372  elicopnf  13373  elxrge0  13385  isprm2  16621  efgrelexlemb  19691  opsrtoslem1  22022  tgphaus  24073  cfilucfil3  25288  ioombl1lem4  25530  vitalilem1  25577  ellogdm  26616  nb3grpr2  29468  upgr2wlk  29752  erclwwlkref  30107  erclwwlknref  30156  0spth  30213  0crct  30220  pjimai  32264  eulerpartlemt0  34547  bnj1101  34961  satfvsuclem2  35576  bj-snglc  37217  bj-epelb  37317  bj-opelidb1  37408  icorempo  37606  wl-cases2-dnf  37767  matunitlindf  37869  disjressuc2  38662  dflim5  43686  pm11.58  44746