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 229	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

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

This theorem is referenced by:  pm4.71ri  560  pm4.24  563  anabs1  658  pm4.45im  824  pm4.45  994  eu6lem  2573  2eu5  2657  rabeqc  3615  dfid2  5482  imadmrn  5968  dff1o2  6705  f12dfv  7126  isof1oidb  7175  isof1oopb  7176  xpsnen  8796  dom0  8841  dfac5lem2  9811  pwfseqlem4  10349  axgroth6  10515  eqreznegel  12603  xrnemnf  12782  xrnepnf  12783  dfrp2  13057  elioopnf  13104  elioomnf  13105  elicopnf  13106  elxrge0  13118  isprm2  16315  efgrelexlemb  19271  opsrtoslem1  21172  tgphaus  23176  cfilucfil3  24389  ioombl1lem4  24630  vitalilem1  24677  ellogdm  25699  nb3grpr2  27653  upgr2wlk  27938  erclwwlkref  28285  erclwwlknref  28334  0spth  28391  0crct  28398  pjimai  30439  eulerpartlemt0  32236  bnj1101  32664  satfvsuclem2  33222  bj-snglc  35086  bj-epelb  35167  bj-opelidb1  35251  icorempo  35449  wl-cases2-dnf  35598  matunitlindf  35702  pm11.58  41897