Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > in2 | Structured version Visualization version Unicode 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 38801 | . 2 |
3 | 2 | dfvd1ir 38789 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wvd1 38785 wvd2 38793 |
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 197 df-an 386 df-vd1 38786 df-vd2 38794 |
This theorem is referenced by: e223 38860 trsspwALT 39045 sspwtr 39048 pwtrVD 39059 pwtrrVD 39060 snssiALTVD 39062 sstrALT2VD 39069 suctrALT2VD 39071 elex2VD 39073 elex22VD 39074 eqsbc3rVD 39075 tpid3gVD 39077 en3lplem1VD 39078 en3lplem2VD 39079 3ornot23VD 39082 orbi1rVD 39083 19.21a3con13vVD 39087 exbirVD 39088 exbiriVD 39089 rspsbc2VD 39090 tratrbVD 39097 syl5impVD 39099 ssralv2VD 39102 imbi12VD 39109 imbi13VD 39110 sbcim2gVD 39111 sbcbiVD 39112 truniALTVD 39114 trintALTVD 39116 onfrALTVD 39127 relopabVD 39137 19.41rgVD 39138 hbimpgVD 39140 ax6e2eqVD 39143 ax6e2ndeqVD 39145 con3ALTVD 39152 |
Copyright terms: Public domain | W3C validator |