New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpbi | GIF 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 186 | . 2 ⊢ (φ → ψ) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ψ |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 |
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 177 |
This theorem is referenced by: pm5.74i 236 notbii 287 pm5.19 349 ori 364 imori 402 pm4.71i 613 pm4.71ri 614 pm5.32i 618 pm3.24 852 pm5.16 860 biluk 899 4exmid 905 dn1 932 3ori 1242 trubifal 1351 nic-dfim 1434 nic-dfneg 1435 nic-mp 1436 nic-mpALT 1437 tbw-negdf 1464 rb-imdf 1515 mpto2 1534 mpto2OLD 1535 mtp-xorOLD 1537 mpgbi 1549 19.35i 1601 19.36i 1872 19.37aiv 1900 sbco 2083 sbidm 2085 axi12 2333 eqcomi 2357 eqtri 2373 eleqtri 2425 neeqtri 2537 necomi 2598 nemtbir 2604 nrex 2716 rexlimi 2731 isseti 2865 vtocl2 2910 vtocl3 2911 eueq1 3009 euxfr2 3021 sseqtri 3303 3sstr3i 3309 pssn2lp 3370 equncomi 3410 unssi 3438 ssini 3478 unabs 3485 inabs 3486 dfin4 3495 npss0 3589 difid 3618 disjdif 3622 difin0 3623 snid 3760 snsssn 3873 iinrab2 4029 rintn0 4056 axxpprim 4090 axcnvprim 4091 axssetprim 4092 axsiprim 4093 axtyplowerprim 4094 axins2prim 4095 axins3prim 4096 iota4an 4358 ltfinirr 4457 evenoddnnnul 4514 evenodddisj 4516 vfinspeqtncv 4553 0cnelphi 4597 copsexg 4607 opeq 4619 breqtri 4662 rn0 4969 dmresi 5004 nfunv 5138 fnopab 5207 xpsn 5435 fvi 5442 fvsnun2 5448 xpnedisj 5513 fnmpti 5690 fmpti 5693 fncup 5813 addcfn 5825 epprc 5827 fncross 5846 fnfullfun 5858 fvfullfun 5864 fnmap 6007 fnpm 6008 dmen 6041 xpsnen 6049 xpcomen 6052 xpassen 6057 enpw1pw 6075 ncpwpw1 6153 ce0addcnnul 6179 sbthlem1 6203 cet 6234 0lt1c 6258 nmembers1lem2 6269 ltcirr 6272 nnc3n3p1 6278 nchoicelem5 6293 fnfreclem2 6318 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |