Theorem a2i 11

Description: Inference derived from axiom ax-2 6. (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 6	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
3	1, 2	ax-mp 7	1 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))

Syntax hints:   → wi 4

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

This theorem is referenced by:  imim2i  12  mpd  13  sylcom  28  pm2.43  52  ancl  311  ancr  314  anc2r  321  pm2.65  617  pm2.18dc  783  con4biddc  787  hbim1  1502  sbcof2  1731  ralimia  2424  ceqsalg  2627  rspct  2694  elabgt  2735  fvmptt  5283  ordiso2  6446  bj-exlimmp  10580  bj-rspgt  10596  bj-indint  10726