![]() |
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 3621 rspc2v 3623 rspc3v 3628 rspc4v 3631 rspc8v 3633 copsexgw 5491 copsexg 5492 chfnrn 7051 fvcofneq 7095 ffnfv 7118 f1elima 7262 onint 7778 peano5 7884 peano5OLD 7885 f1oweALT 7959 smoel2 8363 pssnn 9168 php 9210 pssnnOLD 9265 fiint 9324 dffi2 9418 alephnbtwn 10066 cfcof 10269 zorn2lem7 10497 suplem1pr 11047 addsrpr 11070 mulsrpr 11071 cau3lem 15301 divalglem8 16343 efgi 19587 elfrlmbasn0 21318 locfincmp 23030 tx1stc 23154 fbunfip 23373 filuni 23389 ufileu 23423 rescncf 24413 shmodsi 30642 spanuni 30797 spansneleq 30823 mdi 31548 dmdi 31555 dmdi4 31560 funimass4f 31861 bj-ax89 35555 poimirlem32 36520 ffnafv 45879 |
Copyright terms: Public domain | W3C validator |