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 511 19.38a 1846 ax13lem1 2373 ax13lem2 2375 axc11n 2425 reuss2 4201 reupick 4205 elinxp 5857 ordtr2 6210 suc11 6269 funimass4 6728 fliftfun 7072 omlimcl 8228 nneob 8303 rankwflemb 9288 cflm 9743 domtriomlem 9935 grothomex 10322 sup3 11668 caubnd 14801 fbflim2 22721 ellimc3 24623 usgruspgrb 27118 usgredgsscusgredg 27393 3cyclfrgrrn1 28214 dfon2lem6 33328 opnrebl2 34140 bj-nfimt 34446 axc11n11r 34492 bj-nnf-alrim 34564 stdpc5t 34630 wl-ax13lem1 35277 diaintclN 38684 dibintclN 38793 dihintcl 38970 pm11.71 41537 axc11next 41546 rrx2plord2 45586 |
Copyright terms: Public domain | W3C validator |