![]() |
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 692 nfimt 1966 19.21tOLDOLD 2217 19.21t-1OLD 2353 ax13lem1 2389 ax13lem2 2437 axc11n 2447 axc11nOLD 2448 sbequi 2508 reuss2 4046 reupick 4050 elres 5589 ordtr2 5925 suc11 5988 funimass4 6405 fliftfun 6721 omlimcl 7823 nneob 7897 rankwflemb 8825 cflm 9260 domtriomlem 9452 grothomex 9839 sup3 11168 caubnd 14293 fbflim2 21978 ellimc3 23838 usgruspgrb 26271 usgredgsscusgredg 26561 3cyclfrgrrn1 27435 dfon2lem6 31994 opnrebl2 32618 axc11n11r 32975 stdpc5t 33116 wl-ax13lem1 33596 diaintclN 36845 dibintclN 36954 dihintcl 37131 pm11.71 39095 axc11next 39105 |
Copyright terms: Public domain | W3C validator |