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  53  pm2.18  115  ancl  561  ancr  564  anc2r  571  hbim1  2054  ralimia  2829  ceqsalgALT  3094  rspct  3164  elabgt  3205  fvmptt  6032  tfi  6757  fnfi  7934  finsschain  7966  ordiso2  8113  ordtypelem7  8122  dfom3  8237  infdiffi  8248  cantnfp1lem3  8270  cantnf  8283  r1ordg  8334  ttukeylem6  9029  fpwwe2lem8  9147  wunfi  9231  dfnn2  10711  trclfvcotr  13233  psgnunilem3  17298  pgpfac1  17873  fiuncmp  20576  filssufilg  21084  ufileu  21092  pjnormssi  27984  bnj1110  29943  waj-ax  31223  bj-sb  31465  bj-equsal1  31608  bj-equsal2  31609  rdgeqoa  31994  wl-mps  32064  refimssco  36452  atbiffatnnb  39020