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  660  pm4.45im  826  pm4.45  996  eu6lem  2567  2eu5  2651  rabeqcOLD  3680  dfid2  5575  imadmrn  6067  dff1o2  6835  f12dfv  7267  isof1oidb  7317  isof1oopb  7318  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  19612  opsrtoslem1  21607  tgphaus  23612  cfilucfil3  24828  ioombl1lem4  25069  vitalilem1  25116  ellogdm  26138  nb3grpr2  28629  upgr2wlk  28914  erclwwlkref  29262  erclwwlknref  29311  0spth  29368  0crct  29375  pjimai  31416  eulerpartlemt0  33356  bnj1101  33783  satfvsuclem2  34339  bj-snglc  35838  bj-epelb  35938  bj-opelidb1  36022  icorempo  36220  wl-cases2-dnf  36369  matunitlindf  36474  disjressuc2  37246  dflim5  42064  pm11.58  43134