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  2566  2eu5  2649  rabeqcOLD  3654  dfid2  5528  imadmrn  6030  dff1o2  6787  f12dfv  7230  isof1oidb  7281  isof1oopb  7282  xpsnen  9002  dfac5lem2  10053  axgroth6  10757  eqreznegel  12869  xrnemnf  13053  xrnepnf  13054  dfrp2  13331  elioopnf  13380  elioomnf  13381  elicopnf  13382  elxrge0  13394  isprm2  16628  efgrelexlemb  19656  opsrtoslem1  21938  tgphaus  23980  cfilucfil3  25196  ioombl1lem4  25438  vitalilem1  25485  ellogdm  26524  nb3grpr2  29286  upgr2wlk  29570  erclwwlkref  29922  erclwwlknref  29971  0spth  30028  0crct  30035  pjimai  32078  eulerpartlemt0  34333  bnj1101  34747  satfvsuclem2  35320  bj-snglc  36930  bj-epelb  37030  bj-opelidb1  37114  icorempo  37312  wl-cases2-dnf  37473  matunitlindf  37585  disjressuc2  38347  dflim5  43291  pm11.58  44352