![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e11 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e11.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e11.2 | ⊢ ( 𝜑 ▶ 𝜒 ) |
e11.3 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
e11 | ⊢ ( 𝜑 ▶ 𝜃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e11.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | e11.2 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) | |
3 | e11.3 | . . 3 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
4 | 3 | a1i 11 | . 2 ⊢ (𝜓 → (𝜓 → (𝜒 → 𝜃))) |
5 | 1, 1, 2, 4 | e111 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 |