![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9 | Structured version Visualization version GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
sylan9.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
sylan9.2 | ⊢ (𝜃 → (𝜒 → 𝜏)) |
Ref | Expression |
---|---|
sylan9 | ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | sylan9.2 | . . 3 ⊢ (𝜃 → (𝜒 → 𝜏)) | |
3 | 1, 2 | syl9 77 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
4 | 3 | imp 408 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: ax8 2113 ax9 2121 rspc2 3590 rspc2v 3592 rspc3v 3595 rspc4v 3597 rspc8v 3598 copsexgw 5451 copsexg 5452 chfnrn 7003 fvcofneq 7047 ffnfv 7070 f1elima 7214 onint 7729 peano5 7834 peano5OLD 7835 f1oweALT 7909 smoel2 8313 pssnn 9118 php 9160 pssnnOLD 9215 fiint 9274 dffi2 9367 alephnbtwn 10015 cfcof 10218 zorn2lem7 10446 suplem1pr 10996 addsrpr 11019 mulsrpr 11020 cau3lem 15248 divalglem8 16290 efgi 19509 elfrlmbasn0 21192 locfincmp 22900 tx1stc 23024 fbunfip 23243 filuni 23259 ufileu 23293 rescncf 24283 shmodsi 30380 spanuni 30535 spansneleq 30561 mdi 31286 dmdi 31293 dmdi4 31298 funimass4f 31604 bj-ax89 35195 poimirlem32 36160 ffnafv 45493 |
Copyright terms: Public domain | W3C validator |