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

Theorem e22 28443
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 28408 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28346
This theorem is referenced by:  e22an  28444  e02  28470  e12  28499  e20  28502  e21  28505  sspwtr  28595  pwtrVD  28598  pwtrrVD  28600  elex22VD  28615  tpid3gVD  28618  en3lplem2VD  28620  imbi12VD  28649  truniALTVD  28654  trintALTVD  28656  onfrALTlem3VD  28663  onfrALTlem2VD  28665  a9e2eqVD  28683  a9e2ndeqVD  28685  sb5ALTVD  28689
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 28347
  Copyright terms: Public domain W3C validator