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

Theorem e22 37094
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 37059 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 36991
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 190  df-an 377  df-vd2 36992
This theorem is referenced by:  e22an  37095  e02  37120  e12  37152  e20  37155  e21  37158  sspwtr  37250  pwtrVD  37261  pwtrrVD  37262  elex22VD  37276  tpid3gVD  37279  en3lplem2VD  37281  imbi12VD  37311  truniALTVD  37316  trintALTVD  37318  onfrALTlem3VD  37325  onfrALTlem2VD  37327  ax6e2eqVD  37345  ax6e2ndeqVD  37347  sb5ALTVD  37351
  Copyright terms: Public domain W3C validator