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

Theorem e22 28481
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 28446 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28378
This theorem is referenced by:  e22an  28482  e02  28507  e12  28545  e20  28548  e21  28551  sspwtr  28643  pwtrVD  28646  pwtrrVD  28647  elex22VD  28660  tpid3gVD  28663  en3lplem2VD  28665  imbi12VD  28694  truniALTVD  28699  trintALTVD  28701  onfrALTlem3VD  28708  onfrALTlem2VD  28710  a9e2eqVD  28728  a9e2ndeqVD  28730  sb5ALTVD  28734
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 28379
  Copyright terms: Public domain W3C validator