Theorem pm4.71i 560

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  pm4.71ri  561  pm4.24  564  anabs1  659  pm4.45im  825  pm4.45  995  eu6lem  2573  2eu5  2657  rabeqc  3622  dfid2  5491  imadmrn  5979  dff1o2  6721  f12dfv  7145  isof1oidb  7195  isof1oopb  7196  xpsnen  8842  dom0OLD  8890  dfac5lem2  9880  pwfseqlem4  10418  axgroth6  10584  eqreznegel  12674  xrnemnf  12853  xrnepnf  12854  dfrp2  13128  elioopnf  13175  elioomnf  13176  elicopnf  13177  elxrge0  13189  isprm2  16387  efgrelexlemb  19356  opsrtoslem1  21262  tgphaus  23268  cfilucfil3  24484  ioombl1lem4  24725  vitalilem1  24772  ellogdm  25794  nb3grpr2  27750  upgr2wlk  28036  erclwwlkref  28384  erclwwlknref  28433  0spth  28490  0crct  28497  pjimai  30538  eulerpartlemt0  32336  bnj1101  32764  satfvsuclem2  33322  bj-snglc  35159  bj-epelb  35240  bj-opelidb1  35324  icorempo  35522  wl-cases2-dnf  35671  matunitlindf  35775  pm11.58  42008