![]() |
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 444 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: ax8 2036 ax9 2043 rspc2 3351 rspc3v 3356 trintssOLD 4803 copsexg 4985 chfnrn 6368 fvcofneq 6407 ffnfv 6428 f1elima 6560 onint 7037 peano5 7131 f1oweALT 7194 smoel2 7505 pssnn 8219 fiint 8278 dffi2 8370 alephnbtwn 8932 cfcof 9134 zorn2lem7 9362 suplem1pr 9912 addsrpr 9934 mulsrpr 9935 cau3lem 14138 divalglem8 15170 efgi 18178 elfrlmbasn0 20154 locfincmp 21377 tx1stc 21501 fbunfip 21720 filuni 21736 ufileu 21770 rescncf 22747 shmodsi 28376 spanuni 28531 spansneleq 28557 mdi 29282 dmdi 29289 dmdi4 29294 funimass4f 29565 bj-ax89 32792 wl-ax8clv1 33508 wl-ax8clv2 33511 poimirlem32 33571 ffnafv 41572 |
Copyright terms: Public domain | W3C validator |