Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpbii | Unicode version |
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Ref | Expression |
---|---|
mpbii.min | |
mpbii.maj |
Ref | Expression |
---|---|
mpbii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbii.min | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | mpbii.maj | . 2 | |
4 | 2, 3 | mpbid 146 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.26dc 897 orandc 928 19.9ht 1628 ax11v2 1807 ax11v 1814 ax11ev 1815 equs5or 1817 nfsbxy 1929 nfsbxyt 1930 nfabdw 2325 eqvisset 2732 vtoclgf 2780 vtoclg1f 2781 eueq3dc 2896 mo2icl 2901 csbiegf 3084 un00 3451 sneqr 3735 preqr1 3743 preq12b 3745 prel12 3746 nfopd 3770 ssex 4114 exmidundif 4180 iunpw 4453 nfimad 4950 dfrel2 5049 funsng 5229 cnvresid 5257 nffvd 5493 fnbrfvb 5522 funfvop 5592 acexmidlema 5828 tposf12 6229 supsnti 6962 exmidonfinlem 7141 sucpw1ne3 7180 sucpw1nel3 7181 recidnq 7326 ltaddnq 7340 ltadd1sr 7709 suplocsrlempr 7740 pncan3 8098 divcanap2 8568 ltp1 8731 ltm1 8733 recreclt 8787 nn0ind-raph 9300 2tnp1ge0ge0 10227 fsumcnv 11368 fprodcnv 11556 ef01bndlem 11687 sin01gt0 11692 cos01gt0 11693 ltoddhalfle 11819 bezoutlemnewy 11918 isprm5 12063 tangtx 13326 bdsepnft 13630 bdssex 13645 bj-inex 13650 bj-d0clsepcl 13668 bj-2inf 13681 bj-inf2vnlem2 13714 |
Copyright terms: Public domain | W3C validator |