New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syl2an | GIF version |
Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.) |
Ref | Expression |
---|---|
syl2an.1 | ⊢ (φ → ψ) |
syl2an.2 | ⊢ (τ → χ) |
syl2an.3 | ⊢ ((ψ ∧ χ) → θ) |
Ref | Expression |
---|---|
syl2an | ⊢ ((φ ∧ τ) → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an.2 | . 2 ⊢ (τ → χ) | |
2 | syl2an.1 | . . 3 ⊢ (φ → ψ) | |
3 | syl2an.3 | . . 3 ⊢ ((ψ ∧ χ) → θ) | |
4 | 2, 3 | sylan 457 | . 2 ⊢ ((φ ∧ χ) → θ) |
5 | 1, 4 | sylan2 460 | 1 ⊢ ((φ ∧ τ) → θ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
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 df-an 360 |
This theorem is referenced by: syl2anr 464 anim12i 549 ax11indalem 2197 eqeqan12d 2368 sylan9eq 2405 csbcomg 3159 sylan9ss 3285 ssconb 3399 ineqan12d 3459 ifpr 3774 unexg 4101 opkelopkabg 4245 opkelcokg 4261 opkelimagekg 4271 xpkexg 4288 cokexg 4309 ncfinlower 4483 tfindi 4496 tfinlefin 4502 vfinspsslem1 4550 opexg 4587 copsex2g 4609 breqan12d 4654 coexg 4749 opbrop 4841 dmpropg 5068 xpexg 5114 funssres 5144 fnco 5191 fcnvres 5243 fodmrnu 5277 fvun1 5379 fconst2g 5452 isomin 5496 oveqan12d 5541 ovg 5601 txpexg 5784 cupvalg 5812 pprodexg 5837 ovcross 5845 qsexg 5982 mapvalg 6009 pmvalg 6010 mapsn 6026 xpassen 6057 enmap1lem5 6073 enprmaplem3 6078 ncaddccl 6144 ncdisjeq 6148 ovcelem1 6171 cenc 6181 sbthlem1 6203 sbthlem3 6205 lectr 6211 leconnnc 6218 tlecg 6230 nmembers1lem3 6270 nnc3n3p1 6278 nnc3n3p2 6279 nnc3p1n3p2 6280 nchoicelem5 6293 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |