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 409 | 1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: spimt 2398 euim 2695 axprlem3 5316 limsssuc 7557 tfindsg 7567 findsg 7601 f1oweALT 7665 oaordi 8164 pssnn 8728 inf3lem2 9084 updjudhf 9352 cardlim 9393 ac10ct 9452 cardaleph 9507 cfub 9663 cfcoflem 9686 hsmexlem2 9841 zorn2lem7 9916 pwcfsdom 9997 grur1a 10233 genpcd 10420 supadd 11601 supmul 11605 zeo 12060 uzwo 12303 xrub 12697 iccsupr 12822 reuccatpfxs1lem 14100 climuni 14901 efgi2 18843 opnnei 21720 tgcn 21852 locfincf 22131 uffix 22521 alexsubALTlem2 22648 alexsubALT 22651 metrest 23126 causs 23893 ocin 29065 spanuni 29313 superpos 30123 bnj518 32151 3orel13 32940 trpredmintr 33063 frmin 33077 nndivsub 33798 bj-spimtv 34109 bj-snmoore 34397 cover2 34981 metf1o 35022 sn-axprlem3 39100 intabssd 39876 stoweidlem62 42338 |
Copyright terms: Public domain | W3C validator |