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

Theorem e11 44269
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 44255 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44150
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 206  df-vd1 44151
This theorem is referenced by:  e11an  44270  e01  44272  e10  44275  elex2VD  44419  elex22VD  44420  eqsbc2VD  44421  tpid3gVD  44423  3ornot23VD  44428  orbi1rVD  44429  3orbi123VD  44431  sbc3orgVD  44432  ordelordALTVD  44448  sbcim2gVD  44456  trsbcVD  44458  undif3VD  44463  sbcssgVD  44464  csbingVD  44465  onfrALTVD  44472  csbeq2gVD  44473  csbsngVD  44474  csbxpgVD  44475  csbresgVD  44476  csbrngVD  44477  csbima12gALTVD  44478  csbunigVD  44479  csbfv12gALTVD  44480  19.41rgVD  44483  2pm13.193VD  44484  hbimpgVD  44485  ax6e2eqVD  44488  2uasbanhVD  44492  notnotrALTVD  44496
  Copyright terms: Public domain W3C validator