![]() |
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 147 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm2.26dc 908 orandc 940 19.9ht 1651 ax11v2 1830 ax11v 1837 ax11ev 1838 equs5or 1840 nfsbxy 1952 nfsbxyt 1953 nfabdw 2348 eqvisset 2759 vtoclgf 2807 vtoclg1f 2808 eueq3dc 2923 mo2icl 2928 csbiegf 3112 un00 3481 sneqr 3772 preqr1 3780 preq12b 3782 prel12 3783 nfopd 3807 ssex 4152 exmidundif 4218 iunpw 4492 nfimad 4991 dfrel2 5091 funsng 5274 cnvresid 5302 nffvd 5539 fnbrfvb 5569 funfvop 5641 acexmidlema 5879 tposf12 6284 supsnti 7018 exmidonfinlem 7206 sucpw1ne3 7245 sucpw1nel3 7246 recidnq 7406 ltaddnq 7420 ltadd1sr 7789 suplocsrlempr 7820 pncan3 8179 divcanap2 8651 ltp1 8815 ltm1 8817 recreclt 8871 nn0ind-raph 9384 2tnp1ge0ge0 10315 fsumcnv 11459 fprodcnv 11647 ef01bndlem 11778 sin01gt0 11783 cos01gt0 11784 ltoddhalfle 11912 bezoutlemnewy 12011 isprm5 12156 nmznsg 13113 tangtx 14612 bdsepnft 14992 bdssex 15007 bj-inex 15012 bj-d0clsepcl 15030 bj-2inf 15043 bj-inf2vnlem2 15076 |
Copyright terms: Public domain | W3C validator |