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

Theorem e22 37021
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 36986 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 36918
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 188  df-an 372  df-vd2 36919
This theorem is referenced by:  e22an  37022  e02  37047  e12  37084  e20  37087  e21  37090  sspwtr  37182  pwtrVD  37193  pwtrrVD  37194  elex22VD  37208  tpid3gVD  37211  en3lplem2VD  37213  imbi12VD  37243  truniALTVD  37248  trintALTVD  37250  onfrALTlem3VD  37257  onfrALTlem2VD  37259  ax6e2eqVD  37277  ax6e2ndeqVD  37279  sb5ALTVD  37283
  Copyright terms: Public domain W3C validator