Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl9r | Structured version Visualization version GIF version |
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
syl9r.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl9r.2 | ⊢ (𝜃 → (𝜒 → 𝜏)) |
Ref | Expression |
---|---|
syl9r | ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl9r.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | syl9r.2 | . . 3 ⊢ (𝜃 → (𝜒 → 𝜏)) | |
3 | 1, 2 | syl9 77 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
4 | 3 | com12 32 | 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: peirceroll 85 imim12 105 sylan9r 509 19.38b 1832 ax12v2 2169 fununi 6423 dfimafn 6722 funimass3 6817 isomin 7079 oneqmin 7508 tz7.48lem 8068 fisupg 8755 fiinfg 8952 trcl 9159 coflim 9672 coftr 9684 axdc3lem2 9862 konigthlem 9979 indpi 10318 nnsub 11670 2ndc1stc 21989 kgencn2 22095 tx1stc 22188 filuni 22423 fclscf 22563 alexsubALTlem2 22586 alexsubALTlem3 22587 alexsubALT 22589 lpni 28185 dfimafnf 30310 dfon2lem6 32931 nodenselem8 33093 bj-nnf-exlim 33983 finixpnum 34759 heiborlem4 34975 lncvrelatN 36799 imbi13 40734 dfaimafn 43245 sgoldbeven3prm 43795 |
Copyright terms: Public domain | W3C validator |