ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a2i GIF version

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
StepHypRef Expression
1 a2i.1 . 2 (𝜑 → (𝜓𝜒))
2 ax-2 7 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff set class
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  314  ancr  317  anc2r  324  pm2.65  631  pm2.18dc  823  con4biddc  825  hbim1  1532  sbcof2  1764  ralimia  2468  ceqsalg  2686  rspct  2754  elabgt  2797  fvmptt  5478  ordiso2  6886  bj-exlimmp  12778  bj-rspgt  12795  bj-indint  12931
  Copyright terms: Public domain W3C validator