Theorem pm4.71i 568

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

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

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 401

This theorem is referenced by:  pm4.71ri  569  pm4.24  573  anabs1  674  pm4.45im  840  pm4.45  1013  eu6lem  2601  2eu5  2683  dfid2  5558  imadmrn  6072  dff1o2  6826  f12dfv  7271  isof1oidb  7322  isof1oopb  7323  xpsnen  9045  dfac5lem2  10104  axgroth6  10808  eqreznegel  12953  xrnemnf  13137  xrnepnf  13138  dfrp2  13416  elioopnf  13465  elioomnf  13466  elicopnf  13467  elxrge0  13479  isprm2  16735  efgrelexlemb  19815  opsrtoslem1  22206  tgphaus  24274  cfilucfil3  25479  ioombl1lem4  25720  vitalilem1  25767  ellogdm  26804  nb3grpr2  29733  upgr2wlk  30016  erclwwlkref  30371  erclwwlknref  30420  0spth  30477  0crct  30484  pjimai  32528  eulerpartlemt0  34759  bnj1101  35173  satfvsuclem2  35852  bj-snglc  37605  bj-epelb  37705  bj-opelidb1  37797  icorempo  37997  wl-cases2-dnf  38167  matunitlindf  38269  disjressuc2  39060  dflim5  44056  pm11.58  45100