![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9r | Structured version Visualization version GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
sylan9r.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
sylan9r.2 | ⊢ (𝜃 → (𝜒 → 𝜏)) |
Ref | Expression |
---|---|
sylan9r | ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9r.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | sylan9r.2 | . . 3 ⊢ (𝜃 → (𝜒 → 𝜏)) | |
3 | 1, 2 | syl9r 78 | . 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: spimt 2289 limsssuc 7092 tfindsg 7102 findsg 7135 f1oweALT 7194 oaordi 7671 pssnn 8219 inf3lem2 8564 cardlim 8836 ac10ct 8895 cardaleph 8950 cfub 9109 cfcoflem 9132 hsmexlem2 9287 zorn2lem7 9362 pwcfsdom 9443 grur1a 9679 genpcd 9866 supadd 11029 supmul 11033 zeo 11501 uzwo 11789 xrub 12180 iccsupr 12304 reuccats1lem 13525 climuni 14327 efgi2 18184 opnnei 20972 tgcn 21104 locfincf 21382 uffix 21772 alexsubALTlem2 21899 alexsubALT 21902 metrest 22376 causs 23142 ocin 28283 spanuni 28531 superpos 29341 bnj518 31082 3orel13 31724 trpredmintr 31855 frmin 31867 nndivsub 32581 bj-spimtv 32843 bj-snmoore 33193 cover2 33638 metf1o 33681 intabssd 38233 stoweidlem62 40597 reuccatpfxs1lem 41758 |
Copyright terms: Public domain | W3C validator |