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 1842 ax13lem1 2374 ax13lem2 2376 axc11n 2426 reuss2 4249 reupick 4252 elinxp 5929 ordtr2 6310 suc11 6369 funimass4 6834 fliftfun 7183 omlimcl 8409 nneob 8486 rankwflemb 9551 cflm 10006 domtriomlem 10198 grothomex 10585 sup3 11932 caubnd 15070 fbflim2 23128 ellimc3 25043 usgruspgrb 27551 usgredgsscusgredg 27826 3cyclfrgrrn1 28649 dfon2lem6 33764 opnrebl2 34510 bj-nfimt 34819 axc11n11r 34865 bj-nnf-alrim 34937 stdpc5t 35010 wl-ax13lem1 35665 diaintclN 39072 dibintclN 39181 dihintcl 39358 pm11.71 42015 axc11next 42024 rrx2plord2 46068 |
Copyright terms: Public domain | W3C validator |