Theorem pm4.71i 561

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 559	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	mpbi 229	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  pm4.71ri  562  pm4.24  565  anabs1  661  pm4.45im  827  pm4.45  997  eu6lem  2568  2eu5  2652  rabeqcOLD  3682  dfid2  5577  imadmrn  6070  dff1o2  6839  f12dfv  7271  isof1oidb  7321  isof1oopb  7322  xpsnen  9055  dom0OLD  9103  dfac5lem2  10119  pwfseqlem4  10657  axgroth6  10823  eqreznegel  12918  xrnemnf  13097  xrnepnf  13098  dfrp2  13373  elioopnf  13420  elioomnf  13421  elicopnf  13422  elxrge0  13434  isprm2  16619  efgrelexlemb  19618  opsrtoslem1  21616  tgphaus  23621  cfilucfil3  24837  ioombl1lem4  25078  vitalilem1  25125  ellogdm  26147  nb3grpr2  28671  upgr2wlk  28956  erclwwlkref  29304  erclwwlknref  29353  0spth  29410  0crct  29417  pjimai  31460  eulerpartlemt0  33399  bnj1101  33826  satfvsuclem2  34382  bj-snglc  35898  bj-epelb  35998  bj-opelidb1  36082  icorempo  36280  wl-cases2-dnf  36429  matunitlindf  36534  disjressuc2  37306  dflim5  42127  pm11.58  43197