![]() |
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 506 19.38a 1835 ax13lem1 2368 ax13lem2 2370 axc11n 2420 rspc6v 3628 reuss2 4318 reupick 4321 elinxp 6028 ordtr2 6420 suc11 6483 funimass4 6967 fliftfun 7324 omlimcl 8608 nneob 8686 rankwflemb 9836 cflm 10293 domtriomlem 10485 grothomex 10872 sup3 12223 caubnd 15363 fbflim2 23972 ellimc3 25899 usgruspgrb 29119 usgredgsscusgredg 29396 3cyclfrgrrn1 30218 dfon2lem6 35612 opnrebl2 36033 bj-nfimt 36342 axc11n11r 36388 bj-nnf-alrim 36460 stdpc5t 36532 wl-ax13lem1 37201 diaintclN 40757 dibintclN 40866 dihintcl 41043 sn-sup3d 42252 dflim5 42995 pm11.71 44071 axc11next 44080 rrx2plord2 48110 |
Copyright terms: Public domain | W3C validator |