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  828  pm4.45  1000  eu6lem  2573  2eu5  2656  rabeqcOLD  3690  dfid2  5580  imadmrn  6088  dff1o2  6853  f12dfv  7293  isof1oidb  7344  isof1oopb  7345  xpsnen  9095  dom0OLD  9143  dfac5lem2  10164  axgroth6  10868  eqreznegel  12976  xrnemnf  13159  xrnepnf  13160  dfrp2  13436  elioopnf  13483  elioomnf  13484  elicopnf  13485  elxrge0  13497  isprm2  16719  efgrelexlemb  19768  opsrtoslem1  22079  tgphaus  24125  cfilucfil3  25354  ioombl1lem4  25596  vitalilem1  25643  ellogdm  26681  nb3grpr2  29400  upgr2wlk  29686  erclwwlkref  30039  erclwwlknref  30088  0spth  30145  0crct  30152  pjimai  32195  eulerpartlemt0  34371  bnj1101  34798  satfvsuclem2  35365  bj-snglc  36970  bj-epelb  37070  bj-opelidb1  37154  icorempo  37352  wl-cases2-dnf  37513  matunitlindf  37625  disjressuc2  38389  dflim5  43342  pm11.58  44409