Theorem a2i 11

Description: Inference derived from axiom ax-2 7. (Contributed by NM, 5-Aug-1993.)

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:  imim2i  12  mpd  13  sylcom  28  pm2.43  53  ancl  316  ancr  319  anc2r  326  pm2.65  649  pm2.18dc  841  con4biddc  843  hbim1  1550  sbcof2  1783  ralimia  2496  ceqsalg  2717  rspct  2786  elabgt  2829  fvmptt  5520  ordiso2  6928  bj-exlimmp  13147  bj-rspgt  13164  bj-indint  13300