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

Theorem e10 37073
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  |-  (. ph  ->.  ps
).
e10.2  |-  ch
e10.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
e10  |-  (. ph  ->.  th
).

Proof of Theorem e10
StepHypRef Expression
1 e10.1 . 2  |-  (. ph  ->.  ps
).
2 e10.2 . . 3  |-  ch
32vd01 36976 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 37067 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36939
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 189  df-vd1 36940
This theorem is referenced by:  e10an  37074  en3lpVD  37241  3orbi123VD  37246  sbc3orgVD  37247  exbiriVD  37250  3impexpVD  37252  3impexpbicomVD  37253  al2imVD  37259  equncomVD  37265  trsbcVD  37274  sbcssgVD  37280  csbingVD  37281  onfrALTVD  37288  csbsngVD  37290  csbxpgVD  37291  csbresgVD  37292  csbrngVD  37293  csbima12gALTVD  37294  csbunigVD  37295  csbfv12gALTVD  37296  con5VD  37297  hbimpgVD  37301  hbalgVD  37302  hbexgVD  37303  ax6e2eqVD  37304  ax6e2ndeqVD  37306  e2ebindVD  37309  sb5ALTVD  37310
  Copyright terms: Public domain W3C validator