![]() |
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 3587 rspc2v 3589 rspc3v 3592 copsexgw 5445 copsexg 5446 chfnrn 6995 fvcofneq 7038 ffnfv 7061 f1elima 7205 onint 7716 peano5 7821 peano5OLD 7822 f1oweALT 7896 smoel2 8277 pssnn 9046 php 9088 pssnnOLD 9143 fiint 9202 dffi2 9293 alephnbtwn 9941 cfcof 10144 zorn2lem7 10372 suplem1pr 10922 addsrpr 10945 mulsrpr 10946 cau3lem 15175 divalglem8 16218 efgi 19436 elfrlmbasn0 21098 locfincmp 22805 tx1stc 22929 fbunfip 23148 filuni 23164 ufileu 23198 rescncf 24188 shmodsi 30136 spanuni 30291 spansneleq 30317 mdi 31042 dmdi 31049 dmdi4 31054 funimass4f 31355 bj-ax89 35073 poimirlem32 36041 ffnafv 45194 |
Copyright terms: Public domain | W3C validator |