![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl9r | Structured version Visualization version GIF version |
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
syl9r.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl9r.2 | ⊢ (𝜃 → (𝜒 → 𝜏)) |
Ref | Expression |
---|---|
syl9r | ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl9r.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | syl9r.2 | . . 3 ⊢ (𝜃 → (𝜒 → 𝜏)) | |
3 | 1, 2 | syl9 77 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
4 | 3 | com12 32 | 1 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: peirceroll 85 imim12 105 sylan9r 509 19.38b 1843 ax12v2 2173 fununi 6576 dfimafn 6905 funimass3 7004 isomin 7281 oneqmin 7734 tz7.48lem 8386 fisupg 9234 fiinfg 9434 trcl 9663 coflim 10196 coftr 10208 axdc3lem2 10386 konigthlem 10503 indpi 10842 nnsub 12196 2ndc1stc 22800 kgencn2 22906 tx1stc 22999 filuni 23234 fclscf 23374 alexsubALTlem2 23397 alexsubALTlem3 23398 alexsubALT 23400 nodenselem8 27037 lpni 29369 dfimafnf 31497 dfon2lem6 34303 bj-nnf-exlim 35211 finixpnum 36053 heiborlem4 36263 lncvrelatN 38234 imbi13 42783 dfaimafn 45368 sgoldbeven3prm 45946 |
Copyright terms: Public domain | W3C validator |