Theorem pm4.71i 563

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pm4.71ri  564  pm4.24  567  anabs1  661  pm4.45im  826  pm4.45  995  eu6lem  2633  2eu5  2717  2eu5OLD  2718  rabeqc  3626  imadmrn  5906  dff1o2  6595  f12dfv  7008  isof1oidb  7056  isof1oopb  7057  xpsnen  8584  dom0  8629  dfac5lem2  9535  pwfseqlem4  10073  axgroth6  10239  eqreznegel  12322  xrnemnf  12500  xrnepnf  12501  elioopnf  12821  elioomnf  12822  elicopnf  12823  elxrge0  12835  isprm2  16016  efgrelexlemb  18868  opsrtoslem1  20723  tgphaus  22722  cfilucfil3  23924  ioombl1lem4  24165  vitalilem1  24212  ellogdm  25230  nb3grpr2  27173  upgr2wlk  27458  erclwwlkref  27805  erclwwlknref  27854  0spth  27911  0crct  27918  pjimai  29959  dfrp2  30517  eulerpartlemt0  31737  bnj1101  32166  satfvsuclem2  32720  bj-snglc  34405  bj-epelb  34485  bj-opelidb1  34568  icorempo  34768  wl-cases2-dnf  34917  matunitlindf  35055  pm11.58  41094