Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e11 Structured version   Visualization version   GIF version

Theorem e11 41437
 Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e11.1 (   𝜑   ▶   𝜓   )
e11.2 (   𝜑   ▶   𝜒   )
e11.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
e11 (   𝜑   ▶   𝜃   )

Proof of Theorem e11
StepHypRef Expression
1 e11.1 . 2 (   𝜑   ▶   𝜓   )
2 e11.2 . 2 (   𝜑   ▶   𝜒   )
3 e11.3 . . 3 (𝜓 → (𝜒𝜃))
43a1i 11 . 2 (𝜓 → (𝜓 → (𝜒𝜃)))
51, 1, 2, 4e111 41423 1 (   𝜑   ▶   𝜃   )
 Colors of variables: wff setvar class Syntax hints:   → wi 4  (   wvd1 41318 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 210  df-vd1 41319 This theorem is referenced by:  e11an  41438  e01  41440  e10  41443  elex2VD  41587  elex22VD  41588  eqsbc3rVD  41589  tpid3gVD  41591  3ornot23VD  41596  orbi1rVD  41597  3orbi123VD  41599  sbc3orgVD  41600  ordelordALTVD  41616  sbcim2gVD  41624  trsbcVD  41626  undif3VD  41631  sbcssgVD  41632  csbingVD  41633  onfrALTVD  41640  csbeq2gVD  41641  csbsngVD  41642  csbxpgVD  41643  csbresgVD  41644  csbrngVD  41645  csbima12gALTVD  41646  csbunigVD  41647  csbfv12gALTVD  41648  19.41rgVD  41651  2pm13.193VD  41652  hbimpgVD  41653  ax6e2eqVD  41656  2uasbanhVD  41660  notnotrALTVD  41664
 Copyright terms: Public domain W3C validator