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  2568  2eu5  2651  dfid2  5511  imadmrn  6018  dff1o2  6768  f12dfv  7207  isof1oidb  7258  isof1oopb  7259  xpsnen  8974  dfac5lem2  10015  axgroth6  10719  eqreznegel  12832  xrnemnf  13016  xrnepnf  13017  dfrp2  13294  elioopnf  13343  elioomnf  13344  elicopnf  13345  elxrge0  13357  isprm2  16593  efgrelexlemb  19662  opsrtoslem1  21990  tgphaus  24032  cfilucfil3  25247  ioombl1lem4  25489  vitalilem1  25536  ellogdm  26575  nb3grpr2  29361  upgr2wlk  29645  erclwwlkref  30000  erclwwlknref  30049  0spth  30106  0crct  30113  pjimai  32156  eulerpartlemt0  34382  bnj1101  34796  satfvsuclem2  35404  bj-snglc  37011  bj-epelb  37111  bj-opelidb1  37195  icorempo  37393  wl-cases2-dnf  37554  matunitlindf  37666  disjressuc2  38428  dflim5  43370  pm11.58  44431