| 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 406 | 1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: 3orel13 1489 spimt 2391 euim 2617 ceqsalt 3515 spcimgft 3546 axprlem3OLD 5428 feldmfvelcdm 7106 limsssuc 7871 tfindsg 7882 findsg 7919 f1oweALT 7997 oaordi 8584 pssnn 9208 inf3lem2 9669 updjudhf 9971 cardlim 10012 ac10ct 10074 cardaleph 10129 cfub 10289 cfcoflem 10312 hsmexlem2 10467 zorn2lem7 10542 pwcfsdom 10623 grur1a 10859 genpcd 11046 supadd 12236 supmul 12240 zeo 12704 uzwo 12953 xrub 13354 iccsupr 13482 reuccatpfxs1lem 14784 climuni 15588 efgi2 19743 opnnei 23128 tgcn 23260 locfincf 23539 uffix 23929 alexsubALTlem2 24056 alexsubALT 24059 metrest 24537 causs 25332 ocin 31315 spanuni 31563 superpos 32373 bnj518 34900 nndivsub 36458 bj-spimtv 36795 bj-snmoore 37114 cover2 37722 metf1o 37762 sn-axprlem3 42256 intabssd 43532 relpfrlem 44974 stoweidlem62 46077 pgindnf 49235 |
| Copyright terms: Public domain | W3C validator |