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

Theorem e22 31726
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 31691 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 31623
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 185  df-an 371  df-vd2 31624
This theorem is referenced by:  e22an  31727  e02  31752  e12  31790  e20  31793  e21  31796  sspwtr  31888  pwtrVD  31893  pwtrrVD  31894  elex22VD  31908  tpid3gVD  31911  en3lplem2VD  31913  imbi12VD  31942  truniALTVD  31947  trintALTVD  31949  onfrALTlem3VD  31956  onfrALTlem2VD  31958  ax6e2eqVD  31976  ax6e2ndeqVD  31978  sb5ALTVD  31982
  Copyright terms: Public domain W3C validator