New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syl5ibrcom | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.) |
Ref | Expression |
---|---|
syl5ibr.1 | ⊢ (φ → θ) |
syl5ibr.2 | ⊢ (χ → (ψ ↔ θ)) |
Ref | Expression |
---|---|
syl5ibrcom | ⊢ (φ → (χ → ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ibr.1 | . . 3 ⊢ (φ → θ) | |
2 | syl5ibr.2 | . . 3 ⊢ (χ → (ψ ↔ θ)) | |
3 | 1, 2 | syl5ibr 212 | . 2 ⊢ (χ → (φ → ψ)) |
4 | 3 | com12 27 | 1 ⊢ (φ → (χ → ψ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: biimprcd 216 nfsb4t 2080 elsnc2g 3761 pwadjoin 4119 opkth1g 4130 pw1disj 4167 eqpw1uni 4330 nnc0suc 4412 nndisjeq 4429 leltfintr 4458 lefinlteq 4463 lenltfin 4469 ncfinraise 4481 tfindi 4496 tfinsuc 4498 evenodddisj 4516 nnadjoin 4520 nnpweq 4523 sfinltfin 4535 vfin1cltv 4547 nulnnn 4556 funcnvuni 5161 foco2 5426 fsn 5432 fconst2g 5452 funfvima 5459 fntxp 5804 fnpprod 5843 enadjlem1 6059 enmap2lem3 6065 ncdisjun 6136 dflec2 6210 lectr 6211 leaddc1 6214 tlecg 6229 ce0tb 6237 ce0lenc1 6238 nclenn 6248 addcdi 6249 muc0or 6251 lemuc1 6252 lecadd2 6265 ncslesuc 6266 nmembers1lem3 6269 nncdiv3 6275 nnc3n3p1 6276 nchoicelem1 6287 nchoicelem2 6288 nchoicelem6 6292 |
Copyright terms: Public domain | W3C validator |