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

Theorem e22 28709
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e22.1  |-  (. ph ,. ps  ->.  ch ).
e22.2  |-  (. ph ,. ps  ->.  th ).
e22.3  |-  ( ch 
->  ( th  ->  ta ) )
Assertion
Ref Expression
e22  |-  (. ph ,. ps  ->.  ta ).

Proof of Theorem e22
StepHypRef Expression
1 e22.1 . 2  |-  (. ph ,. ps  ->.  ch ).
2 e22.2 . 2  |-  (. ph ,. ps  ->.  th ).
3 e22.3 . . 3  |-  ( ch 
->  ( th  ->  ta ) )
43a1i 11 . 2  |-  ( ch 
->  ( ch  ->  ( th  ->  ta ) ) )
51, 1, 2, 4e222 28674 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28606
This theorem is referenced by:  e22an  28710  e02  28735  e12  28773  e20  28776  e21  28779  sspwtr  28871  pwtrVD  28874  pwtrrVD  28875  elex22VD  28888  tpid3gVD  28891  en3lplem2VD  28893  imbi12VD  28922  truniALTVD  28927  trintALTVD  28929  onfrALTlem3VD  28936  onfrALTlem2VD  28938  a9e2eqVD  28956  a9e2ndeqVD  28958  sb5ALTVD  28962
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-vd2 28607
  Copyright terms: Public domain W3C validator