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  316  ancr  319  anc2r  326  pm2.65  633  pm2.18dc  825  con4biddc  827  hbim1  1534  sbcof2  1766  ralimia  2470  ceqsalg  2688  rspct  2756  elabgt  2799  fvmptt  5480  ordiso2  6888  bj-exlimmp  12903  bj-rspgt  12920  bj-indint  13056
  Copyright terms: Public domain W3C validator