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 6. (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 6 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
31, 2ax-mp 7 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff set class
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  51  ancl  305  ancr  308  anc2r  315  pm2.65  595  pm2.18dc  761  con4biddc  765  hbim1  1478  sbcof2  1707  ralimia  2399  ceqsalg  2599  rspct  2666  elabgt  2706  fvmptt  5289  ordiso2  6414  bj-exlimmp  10275  bj-rspgt  10291  bj-indint  10421
  Copyright terms: Public domain W3C validator