![]() |
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 407 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: ax8 2112 ax9 2120 rspc2 3589 rspc2v 3591 rspc3v 3594 rspc4v 3596 rspc8v 3597 copsexgw 5452 copsexg 5453 chfnrn 7004 fvcofneq 7048 ffnfv 7071 f1elima 7215 onint 7730 peano5 7835 peano5OLD 7836 f1oweALT 7910 smoel2 8314 pssnn 9119 php 9161 pssnnOLD 9216 fiint 9275 dffi2 9368 alephnbtwn 10016 cfcof 10219 zorn2lem7 10447 suplem1pr 10997 addsrpr 11020 mulsrpr 11021 cau3lem 15251 divalglem8 16293 efgi 19515 elfrlmbasn0 21206 locfincmp 22914 tx1stc 23038 fbunfip 23257 filuni 23273 ufileu 23307 rescncf 24297 shmodsi 30394 spanuni 30549 spansneleq 30575 mdi 31300 dmdi 31307 dmdi4 31312 funimass4f 31618 bj-ax89 35218 poimirlem32 36183 ffnafv 45523 |
Copyright terms: Public domain | W3C validator |