| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl9 | Structured version Visualization version GIF version | ||
| Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
| Ref | Expression |
|---|---|
| syl9.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| syl9.2 | ⊢ (𝜃 → (𝜒 → 𝜏)) |
| Ref | Expression |
|---|---|
| syl9 | ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl9.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | syl9.2 | . . 3 ⊢ (𝜃 → (𝜒 → 𝜏)) | |
| 3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏))) |
| 4 | 1, 3 | syl5d 73 | 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: syl9r 78 com23 86 sylan9 507 19.38a 1840 ax13lem1 2379 ax13lem2 2381 axc11n 2431 rspc6v 3643 reuss2 4326 reupick 4329 elinxp 6037 ordtr2 6428 suc11 6491 funimass4 6973 fliftfun 7332 omlimcl 8616 nneob 8694 rankwflemb 9833 cflm 10290 domtriomlem 10482 grothomex 10869 sup3 12225 caubnd 15397 fbflim2 23985 ellimc3 25914 usgruspgrb 29200 usgredgsscusgredg 29477 3cyclfrgrrn1 30304 dfon2lem6 35789 opnrebl2 36322 bj-nfimt 36639 axc11n11r 36684 bj-nnf-alrim 36756 stdpc5t 36828 wl-ax13lem1 37495 diaintclN 41060 dibintclN 41169 dihintcl 41346 sn-sup3d 42502 dflim5 43342 pm11.71 44416 axc11next 44425 rrx2plord2 48643 |
| Copyright terms: Public domain | W3C validator |