![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbi | Unicode version |
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
mpbi.min |
![]() ![]() |
mpbi.maj |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpbi |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbi.min |
. 2
![]() ![]() | |
2 | mpbi.maj |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpi 113 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | ax-mp 7 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.74i 169 pm4.71i 371 pm4.71ri 372 pm5.32i 427 pm3.24 627 olc 632 orc 633 dn1dc 867 3ori 1195 mptxor 1315 mpgbi 1341 dveeq2 1696 dveeq2or 1697 sbequilem 1719 nfsb 1822 sbco 1842 sbcocom 1844 elsb3 1852 elsb4 1853 hbsbd 1858 dvelimALT 1886 dvelimfv 1887 dvelimor 1894 eqcomi 2044 eqtri 2060 eleqtri 2112 neii 2208 neeqtri 2232 nesymi 2251 necomi 2290 nemtbir 2294 neli 2299 nrex 2411 rexlimi 2426 isseti 2563 eueq1 2713 euxfr2dc 2726 cdeqri 2750 sseqtri 2977 3sstr3i 2983 pssn2lp 3045 equncomi 3089 unssi 3118 ssini 3160 unabs 3167 inabs 3168 ddifss 3175 inssddif 3178 rgenm 3323 snid 3402 rabrsndc 3438 rintm 3744 breqtri 3787 bm1.3ii 3878 zfnuleu 3881 zfpow 3928 copsexg 3981 uniop 3992 pwundifss 4022 onunisuci 4169 zfun 4171 op1stb 4209 op1stbg 4210 ordtriexmidlem 4245 ordtriexmid 4247 ordtri2orexmid 4248 2ordpr 4249 ontr2exmid 4250 onsucsssucexmid 4252 onsucelsucexmid 4255 dtruex 4283 ordsoexmid 4286 0elsucexmid 4289 ordtri2or2exmid 4296 tfi 4305 relop 4486 rn0 4588 dmresi 4661 issref 4707 cnvcnv 4773 rescnvcnv 4783 cnvcnvres 4784 cnvsn 4803 cocnvcnv2 4832 cores2 4833 co01 4835 relcoi1 4849 cnviinm 4859 fnopab 5023 mpt0 5026 fnmpti 5027 f1cnvcnv 5100 f1ovi 5165 fmpti 5321 fvsnun2 5361 oprabss 5590 2nd0 5772 f1stres 5786 f2ndres 5787 reldmtpos 5868 dftpos4 5878 tpostpos 5879 tpos0 5889 smo0 5913 frecfnom 5986 oasuc 6044 ssdomg 6258 xpcomf1o 6299 ssfiexmid 6336 diffitest 6344 card0 6368 dmaddpi 6423 dmmulpi 6424 1lt2pi 6438 1lt2nq 6504 gtso 7097 subf 7213 negne0i 7286 negdii 7295 ltapii 7624 neg1ap0 8026 halflt1 8142 nn0ssz 8263 zeo 8343 numlt 8386 numltc 8387 uzf 8476 indstr 8536 ixxf 8767 iooval2 8784 ioof 8840 unirnioo 8842 fzval2 8877 fzf 8878 fz10 8910 fzpreddisj 8933 4fvwrd4 8997 fzof 9001 fldiv4p1lem1div2 9147 sqrt2gt1lt2 9647 fclim 9815 ex-fl 9895 bdceqi 9963 bdcriota 10003 bdsepnfALT 10009 bdbm1.3ii 10011 bj-d0clsepcl 10049 |
Copyright terms: Public domain | W3C validator |