| Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > in2 | Structured version Visualization version GIF version | ||
| Description: The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| in2.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
| Ref | Expression |
|---|---|
| in2 | ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | in2.1 | . . 3 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
| 2 | 1 | dfvd2i 44605 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3 | 2 | dfvd1ir 44593 | 1 ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ( wvd1 44589 ( wvd2 44597 |
| 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 207 df-an 396 df-vd1 44590 df-vd2 44598 |
| This theorem is referenced by: e223 44655 trsspwALT 44838 sspwtr 44841 pwtrVD 44844 pwtrrVD 44845 snssiALTVD 44847 sstrALT2VD 44854 suctrALT2VD 44856 elex2VD 44858 elex22VD 44859 eqsbc2VD 44860 tpid3gVD 44862 en3lplem1VD 44863 en3lplem2VD 44864 3ornot23VD 44867 orbi1rVD 44868 19.21a3con13vVD 44872 exbirVD 44873 exbiriVD 44874 rspsbc2VD 44875 tratrbVD 44881 syl5impVD 44883 ssralv2VD 44886 imbi12VD 44893 imbi13VD 44894 sbcim2gVD 44895 sbcbiVD 44896 truniALTVD 44898 trintALTVD 44900 onfrALTVD 44911 relopabVD 44921 19.41rgVD 44922 hbimpgVD 44924 ax6e2eqVD 44927 ax6e2ndeqVD 44929 con3ALTVD 44936 |
| Copyright terms: Public domain | W3C validator |