Theorem pm4.71i 562

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm4.71ri  563  pm4.24  566  anabs1  660  pm4.45im  825  pm4.45  994  eu6lem  2658  2eu5  2740  2eu5OLD  2741  rabeqc  3680  imadmrn  5941  dff1o2  6622  f12dfv  7032  isof1oidb  7079  isof1oopb  7080  xpsnen  8603  dom0  8647  dfac5lem2  9552  pwfseqlem4  10086  axgroth6  10252  eqreznegel  12337  xrnemnf  12515  xrnepnf  12516  elioopnf  12834  elioomnf  12835  elicopnf  12836  elxrge0  12848  isprm2  16028  efgrelexlemb  18878  opsrtoslem1  20266  tgphaus  22727  cfilucfil3  23925  ioombl1lem4  24164  vitalilem1  24211  ellogdm  25224  nb3grpr2  27167  upgr2wlk  27452  erclwwlkref  27800  erclwwlknref  27850  0spth  27907  0crct  27914  pjimai  29955  dfrp2  30493  eulerpartlemt0  31629  bnj1101  32058  satfvsuclem2  32609  bj-snglc  34283  bj-epelb  34363  bj-opelidb1  34447  icorempo  34634  wl-cases2-dnf  34754  matunitlindf  34892  pm11.58  40729