![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > in1 | Structured version Visualization version GIF version |
Description: Inference form of df-vd1 40462. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
in1.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
Ref | Expression |
---|---|
in1 | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | in1.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | df-vd1 40462 | . 2 ⊢ (( 𝜑 ▶ 𝜓 ) ↔ (𝜑 → 𝜓)) | |
3 | 1, 2 | mpbi 231 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 40461 |
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 208 df-vd1 40462 |
This theorem is referenced by: vd12 40492 vd13 40493 gen11nv 40509 gen12 40510 exinst11 40518 e1a 40519 el1 40520 e223 40527 e111 40566 e1111 40567 el2122old 40611 el12 40618 el123 40656 un0.1 40671 trsspwALT 40710 sspwtr 40713 pwtrVD 40716 pwtrrVD 40717 snssiALTVD 40719 snsslVD 40721 snelpwrVD 40723 unipwrVD 40724 sstrALT2VD 40726 suctrALT2VD 40728 elex2VD 40730 elex22VD 40731 eqsbc3rVD 40732 zfregs2VD 40733 tpid3gVD 40734 en3lplem1VD 40735 en3lplem2VD 40736 en3lpVD 40737 3ornot23VD 40739 orbi1rVD 40740 3orbi123VD 40742 sbc3orgVD 40743 19.21a3con13vVD 40744 exbirVD 40745 exbiriVD 40746 rspsbc2VD 40747 3impexpVD 40748 3impexpbicomVD 40749 sbcoreleleqVD 40751 tratrbVD 40753 al2imVD 40754 syl5impVD 40755 ssralv2VD 40758 ordelordALTVD 40759 equncomVD 40760 imbi12VD 40765 imbi13VD 40766 sbcim2gVD 40767 sbcbiVD 40768 trsbcVD 40769 truniALTVD 40770 trintALTVD 40772 undif3VD 40774 sbcssgVD 40775 csbingVD 40776 simplbi2comtVD 40780 onfrALTVD 40783 csbeq2gVD 40784 csbsngVD 40785 csbxpgVD 40786 csbresgVD 40787 csbrngVD 40788 csbima12gALTVD 40789 csbunigVD 40790 csbfv12gALTVD 40791 con5VD 40792 relopabVD 40793 19.41rgVD 40794 2pm13.193VD 40795 hbimpgVD 40796 hbalgVD 40797 hbexgVD 40798 ax6e2eqVD 40799 ax6e2ndVD 40800 ax6e2ndeqVD 40801 2sb5ndVD 40802 2uasbanhVD 40803 e2ebindVD 40804 sb5ALTVD 40805 vk15.4jVD 40806 notnotrALTVD 40807 con3ALTVD 40808 sspwimpVD 40811 sspwimpcfVD 40813 suctrALTcfVD 40815 |
Copyright terms: Public domain | W3C validator |