![]() |
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 43434 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | dfvd1ir 43422 | 1 ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43418 ( wvd2 43426 |
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 43419 df-vd2 43427 |
This theorem is referenced by: e223 43484 trsspwALT 43667 sspwtr 43670 pwtrVD 43673 pwtrrVD 43674 snssiALTVD 43676 sstrALT2VD 43683 suctrALT2VD 43685 elex2VD 43687 elex22VD 43688 eqsbc2VD 43689 tpid3gVD 43691 en3lplem1VD 43692 en3lplem2VD 43693 3ornot23VD 43696 orbi1rVD 43697 19.21a3con13vVD 43701 exbirVD 43702 exbiriVD 43703 rspsbc2VD 43704 tratrbVD 43710 syl5impVD 43712 ssralv2VD 43715 imbi12VD 43722 imbi13VD 43723 sbcim2gVD 43724 sbcbiVD 43725 truniALTVD 43727 trintALTVD 43729 onfrALTVD 43740 relopabVD 43750 19.41rgVD 43751 hbimpgVD 43753 ax6e2eqVD 43756 ax6e2ndeqVD 43758 con3ALTVD 43765 |
Copyright terms: Public domain | W3C validator |