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 508 19.38a 1831 ax13lem1 2383 ax13lem2 2385 axc11n 2440 sbequiOLD 2527 sbequiALT 2589 reuss2 4280 reupick 4284 elinxp 5883 ordtr2 6228 suc11 6287 funimass4 6723 fliftfun 7054 omlimcl 8193 nneob 8268 rankwflemb 9210 cflm 9660 domtriomlem 9852 grothomex 10239 sup3 11586 caubnd 14706 fbflim2 22513 ellimc3 24404 usgruspgrb 26893 usgredgsscusgredg 27168 3cyclfrgrrn1 27991 dfon2lem6 32930 opnrebl2 33566 bj-nfimt 33868 axc11n11r 33914 bj-nnf-alrim 33981 stdpc5t 34047 wl-ax13lem1 34628 diaintclN 38074 dibintclN 38183 dihintcl 38360 pm11.71 40606 axc11next 40615 rrx2plord2 44637 |
Copyright terms: Public domain | W3C validator |