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  318  ancr  321  anc2r  328  pm2.65  661  pm2.18dc  857  con4biddc  859  hbim1  1594  sbcof2  1834  ralimia  2568  ceqsalg  2802  rspct  2874  elabgt  2918  fvmptt  5683  ordiso2  7151  bj-exlimmp  15839  bj-rspgt  15856  bj-indint  16001