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

Theorem e22 33836
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 33801 1  |-  (. ph ,. ps  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 33733
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 369  df-vd2 33734
This theorem is referenced by:  e22an  33837  e02  33862  e12  33900  e20  33903  e21  33906  sspwtr  33998  pwtrVD  34009  pwtrrVD  34010  elex22VD  34024  tpid3gVD  34027  en3lplem2VD  34029  imbi12VD  34059  truniALTVD  34064  trintALTVD  34066  onfrALTlem3VD  34073  onfrALTlem2VD  34075  ax6e2eqVD  34093  ax6e2ndeqVD  34095  sb5ALTVD  34099
  Copyright terms: Public domain W3C validator