Theorem pm4.71i 564

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm4.71ri  565  pm4.24  568  anabs1  668  pm4.45im  833  pm4.45  1005  eu6lem  2577  2eu5  2659  dfid2  5515  imadmrn  6022  dff1o2  6772  f12dfv  7217  isof1oidb  7268  isof1oopb  7269  xpsnen  8989  dfac5lem2  10037  axgroth6  10742  eqreznegel  12875  xrnemnf  13059  xrnepnf  13060  dfrp2  13338  elioopnf  13387  elioomnf  13388  elicopnf  13389  elxrge0  13401  isprm2  16642  efgrelexlemb  19716  opsrtoslem1  22031  tgphaus  24100  cfilucfil3  25305  ioombl1lem4  25546  vitalilem1  25593  ellogdm  26621  nb3grpr2  29470  upgr2wlk  29753  erclwwlkref  30108  erclwwlknref  30157  0spth  30214  0crct  30221  pjimai  32265  eulerpartlemt0  34553  bnj1101  34967  satfvsuclem2  35588  bj-snglc  37322  bj-epelb  37422  bj-opelidb1  37513  icorempo  37713  wl-cases2-dnf  37883  matunitlindf  37985  disjressuc2  38778  dflim5  43774  pm11.58  44834