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 40561
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 40547 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 40442
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 208  df-vd1 40443
This theorem is referenced by:  e11an  40562  e01  40564  e10  40567  elex2VD  40711  elex22VD  40712  eqsbc3rVD  40713  tpid3gVD  40715  3ornot23VD  40720  orbi1rVD  40721  3orbi123VD  40723  sbc3orgVD  40724  ordelordALTVD  40740  sbcim2gVD  40748  trsbcVD  40750  undif3VD  40755  sbcssgVD  40756  csbingVD  40757  onfrALTVD  40764  csbeq2gVD  40765  csbsngVD  40766  csbxpgVD  40767  csbresgVD  40768  csbrngVD  40769  csbima12gALTVD  40770  csbunigVD  40771  csbfv12gALTVD  40772  19.41rgVD  40775  2pm13.193VD  40776  hbimpgVD  40777  ax6e2eqVD  40780  2uasbanhVD  40784  notnotrALTVD  40788
  Copyright terms: Public domain W3C validator