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  2566  2eu5  2649  rabeqcOLD  3646  dfid2  5516  imadmrn  6021  dff1o2  6769  f12dfv  7210  isof1oidb  7261  isof1oopb  7262  xpsnen  8978  dfac5lem2  10018  axgroth6  10722  eqreznegel  12835  xrnemnf  13019  xrnepnf  13020  dfrp2  13297  elioopnf  13346  elioomnf  13347  elicopnf  13348  elxrge0  13360  isprm2  16593  efgrelexlemb  19629  opsrtoslem1  21960  tgphaus  24002  cfilucfil3  25218  ioombl1lem4  25460  vitalilem1  25507  ellogdm  26546  nb3grpr2  29328  upgr2wlk  29612  erclwwlkref  29964  erclwwlknref  30013  0spth  30070  0crct  30077  pjimai  32120  eulerpartlemt0  34337  bnj1101  34751  satfvsuclem2  35333  bj-snglc  36943  bj-epelb  37043  bj-opelidb1  37127  icorempo  37325  wl-cases2-dnf  37486  matunitlindf  37598  disjressuc2  38360  dflim5  43302  pm11.58  44363