Theorem pm4.71i 562

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm4.71ri  563  pm4.24  566  anabs1  660  pm4.45im  825  pm4.45  994  eu6lem  2654  2eu5  2738  2eu5OLD  2739  rabeqc  3678  imadmrn  5934  dff1o2  6615  f12dfv  7024  isof1oidb  7071  isof1oopb  7072  xpsnen  8595  dom0  8639  dfac5lem2  9544  pwfseqlem4  10078  axgroth6  10244  eqreznegel  12328  xrnemnf  12506  xrnepnf  12507  elioopnf  12825  elioomnf  12826  elicopnf  12827  elxrge0  12839  isprm2  16020  efgrelexlemb  18870  opsrtoslem1  20258  tgphaus  22719  cfilucfil3  23917  ioombl1lem4  24156  vitalilem1  24203  ellogdm  25216  nb3grpr2  27159  upgr2wlk  27444  erclwwlkref  27792  erclwwlknref  27842  0spth  27899  0crct  27906  pjimai  29947  dfrp2  30485  eulerpartlemt0  31622  bnj1101  32051  satfvsuclem2  32602  bj-snglc  34276  bj-epelb  34355  bj-opelidb1  34439  icorempo  34626  wl-cases2-dnf  34746  matunitlindf  34884  pm11.58  40715