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

Theorem e22 28114
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 28079 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28011
This theorem is referenced by:  e22an  28115  e02  28140  e12  28178  e20  28181  e21  28184  sspwtr  28276  pwtrVD  28279  pwtrrVD  28280  elex22VD  28293  tpid3gVD  28296  en3lplem2VD  28298  imbi12VD  28327  truniALTVD  28332  trintALTVD  28334  onfrALTlem3VD  28341  onfrALTlem2VD  28343  a9e2eqVD  28361  a9e2ndeqVD  28363  sb5ALTVD  28367
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 28012
  Copyright terms: Public domain W3C validator