Theorem a2i 15

Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 16. (Contributed by NM, 29-Dec-1992.)

Hypothesis

Ref	Expression
a2i.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
a2i	⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

Proof of Theorem a2i

Step	Hyp	Ref	Expression
1		a2i.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		ax-2 7	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used by:  mpd  16  imim2i  17  sylcom  31  pm2.43  57  ancl  554  ancr  556  anc2r  564  hbim1  2330  ralimia  3096  ceqsalgALT  3486  rspct  3562  fvmptt  7014  tfi  7864  fnfi  9196  finsschain  9351  ordiso2  9512  ordtypelem7  9521  dfom3  9651  infdiffi  9662  cantnfp1lem3  9684  cantnf  9697  r1ordg  9788  ttukeylem6  10595  fpwwe2lem7  10725  wunfi  10809  dfnn2  12351  trclfvcotr  15167  psgnunilem3  19715  pgpfac1  20301  fiuncmp  23727  filssufilg  24235  ufileu  24243  dfn0s2  28723  pjnormssi  32775  bnj1110  35658  waj-ax  37294  bj-nnclav  37503  bj-sb  37681  bj-equsal1  37828  bj-equsal2  37829  rdgeqoa  38386  wl-mps  38532  refimssco  44700  dfbi1ALTa  46022  simprimi  46023  atbiffatnnb  48075  rexrsb  48263  elsetrecslem  50960