Theorem a2i 14

Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 15. (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 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  mpd  15  imim2i  16  sylcom  30  pm2.43  56  ancl  544  ancr  546  anc2r  554  hbim1  2304  ralimia  3072  ceqsalgALT  3467  rspct  3551  fvmptt  6962  tfi  7797  fnfi  9105  imafiOLD  9219  finsschain  9262  ordiso2  9423  ordtypelem7  9432  dfom3  9559  infdiffi  9570  cantnfp1lem3  9592  cantnf  9605  r1ordg  9693  ttukeylem6  10427  fpwwe2lem7  10551  wunfi  10635  dfnn2  12178  trclfvcotr  14962  psgnunilem3  19462  pgpfac1  20048  fiuncmp  23379  filssufilg  23886  ufileu  23894  dfn0s2  28338  pjnormssi  32254  bnj1110  35140  waj-ax  36612  bj-nnclav  36822  bj-sb  37000  bj-equsal1  37147  bj-equsal2  37148  rdgeqoa  37700  wl-mps  37846  refimssco  44052  dfbi1ALTa  45384  simprimi  45385  natlocalincr  47322  atbiffatnnb  47372  rexrsb  47560  elsetrecslem  50186