| 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 508 19.38b 1841 ax12v2 2179 axprlem3 5425 fununi 6641 dfimafn 6971 funimass3 7074 isomin 7357 oneqmin 7820 tz7.48lem 8481 fisupg 9324 fiinfg 9539 trcl 9768 coflim 10301 coftr 10313 axdc3lem2 10491 konigthlem 10608 indpi 10947 nnsub 12310 2ndc1stc 23459 kgencn2 23565 tx1stc 23658 filuni 23893 fclscf 24033 alexsubALTlem2 24056 alexsubALTlem3 24057 alexsubALT 24059 nodenselem8 27736 n0subs 28360 lpni 30499 dfimafnf 32646 dfon2lem6 35789 bj-nnf-exlim 36757 finixpnum 37612 heiborlem4 37821 lncvrelatN 39783 imbi13 44540 relpmin 44973 dfaimafn 47177 sgoldbeven3prm 47770 |
| Copyright terms: Public domain | W3C validator |