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  3657  dfid2  5535  imadmrn  6041  dff1o2  6805  f12dfv  7248  isof1oidb  7299  isof1oopb  7300  xpsnen  9025  dfac5lem2  10077  axgroth6  10781  eqreznegel  12893  xrnemnf  13077  xrnepnf  13078  dfrp2  13355  elioopnf  13404  elioomnf  13405  elicopnf  13406  elxrge0  13418  isprm2  16652  efgrelexlemb  19680  opsrtoslem1  21962  tgphaus  24004  cfilucfil3  25220  ioombl1lem4  25462  vitalilem1  25509  ellogdm  26548  nb3grpr2  29310  upgr2wlk  29596  erclwwlkref  29949  erclwwlknref  29998  0spth  30055  0crct  30062  pjimai  32105  eulerpartlemt0  34360  bnj1101  34774  satfvsuclem2  35347  bj-snglc  36957  bj-epelb  37057  bj-opelidb1  37141  icorempo  37339  wl-cases2-dnf  37500  matunitlindf  37612  disjressuc2  38374  dflim5  43318  pm11.58  44379