New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sylbi | GIF version |
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sylbi.1 | ⊢ (φ ↔ ψ) |
sylbi.2 | ⊢ (ψ → χ) |
Ref | Expression |
---|---|
sylbi | ⊢ (φ → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbi.1 | . . 3 ⊢ (φ ↔ ψ) | |
2 | 1 | biimpi 186 | . 2 ⊢ (φ → ψ) |
3 | sylbi.2 | . 2 ⊢ (ψ → χ) | |
4 | 2, 3 | syl 15 | 1 ⊢ (φ → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ 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: bi2 189 3imtr4i 257 sylnbi 297 imp 418 an12s 776 an32s 779 an4s 799 oibabs 851 3simpb 953 3simpc 954 3imp 1145 3com12 1155 3com13 1156 syl3anb 1225 19.33b 1608 exintrbi 1613 ax17e 1618 spimfw 1646 a6e 1751 nfr 1761 19.9t 1779 nfnd 1791 nfndOLD 1792 equs5e 1888 exdistrf 1971 equvini 1987 equveli 1988 ax10-16 2190 euex 2227 eumo0 2228 mopick 2266 2euex 2276 2mo 2282 2eu3 2286 exists2 2294 eqcoms 2356 eleq2s 2445 nfcr 2481 necon3bi 2557 necon1ai 2558 necon2ai 2561 pm2.61ne 2591 pm2.61ine 2592 rexex 2673 rsp 2674 ralim 2685 r19.36av 2759 r19.37 2760 r19.44av 2767 r19.45av 2768 gencl 2887 gencbvex 2901 vtoclgf 2913 pm13.183 2979 mo2icl 3015 mob2 3016 reu3 3026 rmoim 3035 2reuswap 3038 sbcex 3055 ra5 3130 sseq1 3292 unineq 3505 dfrab3ss 3533 reldisj 3594 disjel 3597 pssdif 3612 difin0ss 3616 uneqdifeq 3638 r19.2z 3639 r19.3rz 3641 r19.3rzv 3643 ralidm 3653 ifnefalse 3670 ifbi 3679 nelpri 3754 difprsn2 3848 diftpsn3 3849 pwpw0 3855 ssunsn2 3865 snsssn 3873 pwsnALT 3882 intmin4 3955 dfiin2g 4000 iinss2 4018 unipw 4117 pwadjoin 4119 preqr2 4125 preq12b 4127 opkthg 4131 pw10 4161 pw10b 4166 pw1disj 4167 pw1ss 4169 sikss1c1c 4267 opkelimagekg 4271 ins2kss 4279 ins3kss 4280 cokrelk 4284 eqpw1uni 4330 pw1eqadj 4332 euabex 4334 iotauni 4351 iota1 4353 iota4 4357 reiotacl2 4363 dfiota4 4372 0nelsuc 4400 nndisjeq 4429 snfi 4431 lefinlteq 4463 ssfin 4470 tfinprop 4489 evenoddnnnul 4514 evenodddisj 4516 sfin112 4529 sfintfin 4532 sfinltfin 4535 sfin111 4536 spfinsfincl 4539 vfinspnn 4541 vfinspsslem1 4550 copsexg 4607 ralxpf 4827 optocl 4838 breldm 4911 proj1eldm 4927 dmcoss 4971 xpnz 5045 xp11 5056 xpcan 5057 xpcan2 5058 dfco2a 5081 cores2 5091 dfxp2 5113 dffun8 5134 fununi 5160 imadif 5171 fneu 5187 ffoss 5314 f1o00 5317 fo00 5318 nfunsn 5353 fvun1 5379 fvimacnv 5403 unpreima 5408 inpreima 5409 respreima 5410 fvpr1 5449 1stfo 5505 2ndfo 5506 xpnedisj 5513 1st2nd2 5516 oprabid 5550 oprssdm 5612 fvmptss 5705 fvmptss2 5725 op1st2nd 5790 oqelins4 5794 addcfnex 5824 pw1fnf1o 5855 clos1nrel 5886 weds 5938 ecexr 5950 mapprc 6004 mapsspm 6021 mapsspw 6022 map0b 6024 map0 6025 ensymi 6036 entr 6038 idssen 6040 en0 6042 fundmen 6043 xpen 6055 enpw1 6062 enmap2 6068 enmap1 6074 enprmaplem3 6078 nenpw1pwlem2 6085 ncseqnc 6128 muccl 6132 muccom 6134 mucass 6135 1cnc 6139 muc0 6142 mucid1 6143 ncdisjeq 6148 tcdi 6164 sbthlem3 6205 addlec 6208 nc0le1 6216 dflec3 6221 nclenc 6222 lenc 6223 tc11 6228 taddc 6229 letc 6231 ce2le 6233 cet 6234 te0c 6237 ce0lenc1 6239 tlenc1c 6240 addcdi 6250 muc0or 6252 nchoicelem8 6296 nchoicelem12 6300 nchoicelem14 6302 frecxp 6314 scancan 6331 |
Copyright terms: Public domain | W3C validator |