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 41876 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | dfvd1ir 41864 | 1 ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 41860 ( wvd2 41868 |
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 210 df-an 400 df-vd1 41861 df-vd2 41869 |
This theorem is referenced by: e223 41926 trsspwALT 42109 sspwtr 42112 pwtrVD 42115 pwtrrVD 42116 snssiALTVD 42118 sstrALT2VD 42125 suctrALT2VD 42127 elex2VD 42129 elex22VD 42130 eqsbc3rVD 42131 tpid3gVD 42133 en3lplem1VD 42134 en3lplem2VD 42135 3ornot23VD 42138 orbi1rVD 42139 19.21a3con13vVD 42143 exbirVD 42144 exbiriVD 42145 rspsbc2VD 42146 tratrbVD 42152 syl5impVD 42154 ssralv2VD 42157 imbi12VD 42164 imbi13VD 42165 sbcim2gVD 42166 sbcbiVD 42167 truniALTVD 42169 trintALTVD 42171 onfrALTVD 42182 relopabVD 42192 19.41rgVD 42193 hbimpgVD 42195 ax6e2eqVD 42198 ax6e2ndeqVD 42200 con3ALTVD 42207 |
Copyright terms: Public domain | W3C validator |