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  662  pm4.45im  827  pm4.45  999  eu6lem  2572  2eu5  2655  rabeqcOLD  3669  dfid2  5550  imadmrn  6057  dff1o2  6823  f12dfv  7266  isof1oidb  7317  isof1oopb  7318  xpsnen  9069  dom0OLD  9117  dfac5lem2  10138  axgroth6  10842  eqreznegel  12950  xrnemnf  13133  xrnepnf  13134  dfrp2  13411  elioopnf  13460  elioomnf  13461  elicopnf  13462  elxrge0  13474  isprm2  16701  efgrelexlemb  19731  opsrtoslem1  22013  tgphaus  24055  cfilucfil3  25272  ioombl1lem4  25514  vitalilem1  25561  ellogdm  26600  nb3grpr2  29362  upgr2wlk  29648  erclwwlkref  30001  erclwwlknref  30050  0spth  30107  0crct  30114  pjimai  32157  eulerpartlemt0  34401  bnj1101  34815  satfvsuclem2  35382  bj-snglc  36987  bj-epelb  37087  bj-opelidb1  37171  icorempo  37369  wl-cases2-dnf  37530  matunitlindf  37642  disjressuc2  38406  dflim5  43353  pm11.58  44414