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

Theorem e22 28748
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 10 . 2  |-  ( ch 
->  ( ch  ->  ( th  ->  ta ) ) )
51, 1, 2, 4e222 28713 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28645
This theorem is referenced by:  e22an  28749  e02  28775  e12  28813  e20  28816  e21  28819  sspwtr  28911  pwtrVD  28914  pwtrrVD  28916  elex22VD  28931  tpid3gVD  28934  en3lplem2VD  28936  imbi12VD  28965  truniALTVD  28970  trintALTVD  28972  onfrALTlem3VD  28979  onfrALTlem2VD  28981  a9e2eqVD  28999  a9e2ndeqVD  29001  sb5ALTVD  29005
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 177  df-an 360  df-vd2 28646
  Copyright terms: Public domain W3C validator