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  2573  2eu5  2656  dfid2  5521  imadmrn  6029  dff1o2  6779  f12dfv  7219  isof1oidb  7270  isof1oopb  7271  xpsnen  8989  dfac5lem2  10034  axgroth6  10739  eqreznegel  12847  xrnemnf  13031  xrnepnf  13032  dfrp2  13310  elioopnf  13359  elioomnf  13360  elicopnf  13361  elxrge0  13373  isprm2  16609  efgrelexlemb  19679  opsrtoslem1  22010  tgphaus  24061  cfilucfil3  25276  ioombl1lem4  25518  vitalilem1  25565  ellogdm  26604  nb3grpr2  29456  upgr2wlk  29740  erclwwlkref  30095  erclwwlknref  30144  0spth  30201  0crct  30208  pjimai  32251  eulerpartlemt0  34526  bnj1101  34940  satfvsuclem2  35554  bj-snglc  37170  bj-epelb  37270  bj-opelidb1  37358  icorempo  37556  wl-cases2-dnf  37717  matunitlindf  37819  disjressuc2  38596  dflim5  43571  pm11.58  44631