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 43449
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 43435 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 43330
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 43331
This theorem is referenced by:  e11an  43450  e01  43452  e10  43455  elex2VD  43599  elex22VD  43600  eqsbc2VD  43601  tpid3gVD  43603  3ornot23VD  43608  orbi1rVD  43609  3orbi123VD  43611  sbc3orgVD  43612  ordelordALTVD  43628  sbcim2gVD  43636  trsbcVD  43638  undif3VD  43643  sbcssgVD  43644  csbingVD  43645  onfrALTVD  43652  csbeq2gVD  43653  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbima12gALTVD  43658  csbunigVD  43659  csbfv12gALTVD  43660  19.41rgVD  43663  2pm13.193VD  43664  hbimpgVD  43665  ax6e2eqVD  43668  2uasbanhVD  43672  notnotrALTVD  43676
  Copyright terms: Public domain W3C validator