![]() |
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 503 19.38a 1938 ax13lem1 2391 ax13lem2 2393 axc11n 2447 sbequi 2506 reuss2 4136 reupick 4140 elinxp 5670 elresOLD 5672 ordtr2 6007 suc11 6066 funimass4 6494 fliftfun 6817 omlimcl 7925 nneob 7999 rankwflemb 8933 cflm 9387 domtriomlem 9579 grothomex 9966 sup3 11310 caubnd 14475 fbflim2 22151 ellimc3 24042 usgruspgrb 26480 usgredgsscusgredg 26757 3cyclfrgrrn1 27655 dfon2lem6 32220 opnrebl2 32843 bj-exlalrim 33122 bj-nfimt 33135 axc11n11r 33201 stdpc5t 33331 wl-ax13lem1 33827 diaintclN 37126 dibintclN 37235 dihintcl 37412 pm11.71 39430 axc11next 39439 |
Copyright terms: Public domain | W3C validator |