Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e10 Structured version   Visualization version   GIF version

Theorem e10 37940
Description: A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e10.1 (   𝜑   ▶   𝜓   )
e10.2 𝜒
e10.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
e10 (   𝜑   ▶   𝜃   )

Proof of Theorem e10
StepHypRef Expression
1 e10.1 . 2 (   𝜑   ▶   𝜓   )
2 e10.2 . . 3 𝜒
32vd01 37843 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 37934 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 37806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 196  df-vd1 37807
This theorem is referenced by:  e10an  37941  en3lpVD  38102  3orbi123VD  38107  sbc3orgVD  38108  exbiriVD  38111  3impexpVD  38113  3impexpbicomVD  38114  al2imVD  38120  equncomVD  38126  trsbcVD  38135  sbcssgVD  38141  csbingVD  38142  onfrALTVD  38149  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  con5VD  38158  hbimpgVD  38162  hbalgVD  38163  hbexgVD  38164  ax6e2eqVD  38165  ax6e2ndeqVD  38167  e2ebindVD  38170  sb5ALTVD  38171
  Copyright terms: Public domain W3C validator