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  663  pm4.45im  828  pm4.45  1000  eu6lem  2573  2eu5  2656  dfid2  5528  imadmrn  6035  dff1o2  6785  f12dfv  7228  isof1oidb  7279  isof1oopb  7280  xpsnen  8999  dfac5lem2  10046  axgroth6  10751  eqreznegel  12884  xrnemnf  13068  xrnepnf  13069  dfrp2  13347  elioopnf  13396  elioomnf  13397  elicopnf  13398  elxrge0  13410  isprm2  16651  efgrelexlemb  19725  opsrtoslem1  22033  tgphaus  24082  cfilucfil3  25287  ioombl1lem4  25528  vitalilem1  25575  ellogdm  26603  nb3grpr2  29452  upgr2wlk  29735  erclwwlkref  30090  erclwwlknref  30139  0spth  30196  0crct  30203  pjimai  32247  eulerpartlemt0  34513  bnj1101  34927  satfvsuclem2  35542  bj-snglc  37276  bj-epelb  37376  bj-opelidb1  37467  icorempo  37667  wl-cases2-dnf  37837  matunitlindf  37939  disjressuc2  38732  dflim5  43757  pm11.58  44817