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  661  pm4.45im  827  pm4.45  998  eu6lem  2576  2eu5  2659  rabeqcOLD  3706  dfid2  5595  imadmrn  6099  dff1o2  6867  f12dfv  7309  isof1oidb  7360  isof1oopb  7361  xpsnen  9121  dom0OLD  9169  dfac5lem2  10193  axgroth6  10897  eqreznegel  12999  xrnemnf  13180  xrnepnf  13181  dfrp2  13456  elioopnf  13503  elioomnf  13504  elicopnf  13505  elxrge0  13517  isprm2  16729  efgrelexlemb  19792  opsrtoslem1  22102  tgphaus  24146  cfilucfil3  25373  ioombl1lem4  25615  vitalilem1  25662  ellogdm  26699  nb3grpr2  29418  upgr2wlk  29704  erclwwlkref  30052  erclwwlknref  30101  0spth  30158  0crct  30165  pjimai  32208  eulerpartlemt0  34334  bnj1101  34760  satfvsuclem2  35328  bj-snglc  36935  bj-epelb  37035  bj-opelidb1  37119  icorempo  37317  wl-cases2-dnf  37466  matunitlindf  37578  disjressuc2  38344  dflim5  43291  pm11.58  44359