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 40899
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 40885 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 40780
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 40781
This theorem is referenced by:  e11an  40900  e01  40902  e10  40905  elex2VD  41049  elex22VD  41050  eqsbc3rVD  41051  tpid3gVD  41053  3ornot23VD  41058  orbi1rVD  41059  3orbi123VD  41061  sbc3orgVD  41062  ordelordALTVD  41078  sbcim2gVD  41086  trsbcVD  41088  undif3VD  41093  sbcssgVD  41094  csbingVD  41095  onfrALTVD  41102  csbeq2gVD  41103  csbsngVD  41104  csbxpgVD  41105  csbresgVD  41106  csbrngVD  41107  csbima12gALTVD  41108  csbunigVD  41109  csbfv12gALTVD  41110  19.41rgVD  41113  2pm13.193VD  41114  hbimpgVD  41115  ax6e2eqVD  41118  2uasbanhVD  41122  notnotrALTVD  41126
  Copyright terms: Public domain W3C validator