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

Theorem e11 37934
 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 37920 1 (   𝜑   ▶   𝜃   )
 Colors of variables: wff setvar class Syntax hints:   → wi 4  (   wvd1 37806 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 196  df-vd1 37807 This theorem is referenced by:  e11an  37935  e01  37937  e10  37940  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  tpid3gVD  38099  3ornot23VD  38104  orbi1rVD  38105  3orbi123VD  38107  sbc3orgVD  38108  sbcoreleleqVD  38117  ordelordALTVD  38125  sbcim2gVD  38133  trsbcVD  38135  undif3VD  38140  sbcssgVD  38141  csbingVD  38142  onfrALTVD  38149  csbeq2gVD  38150  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  19.41rgVD  38160  2pm13.193VD  38161  hbimpgVD  38162  ax6e2eqVD  38165  2uasbanhVD  38169  notnotrALTVD  38173
 Copyright terms: Public domain W3C validator