![]() |
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 43331 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | dfvd1ir 43319 | 1 ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43315 ( wvd2 43323 |
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-an 397 df-vd1 43316 df-vd2 43324 |
This theorem is referenced by: e223 43381 trsspwALT 43564 sspwtr 43567 pwtrVD 43570 pwtrrVD 43571 snssiALTVD 43573 sstrALT2VD 43580 suctrALT2VD 43582 elex2VD 43584 elex22VD 43585 eqsbc2VD 43586 tpid3gVD 43588 en3lplem1VD 43589 en3lplem2VD 43590 3ornot23VD 43593 orbi1rVD 43594 19.21a3con13vVD 43598 exbirVD 43599 exbiriVD 43600 rspsbc2VD 43601 tratrbVD 43607 syl5impVD 43609 ssralv2VD 43612 imbi12VD 43619 imbi13VD 43620 sbcim2gVD 43621 sbcbiVD 43622 truniALTVD 43624 trintALTVD 43626 onfrALTVD 43637 relopabVD 43647 19.41rgVD 43648 hbimpgVD 43650 ax6e2eqVD 43653 ax6e2ndeqVD 43655 con3ALTVD 43662 |
Copyright terms: Public domain | W3C validator |