![]() |
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: sylan9r 693 ax12v2 2198 nfimdOLD 2371 fununi 6125 dfimafn 6408 funimass3 6497 isomin 6751 oneqmin 7171 tz7.48lem 7706 fisupg 8375 fiinfg 8572 trcl 8779 coflim 9295 coftr 9307 axdc3lem2 9485 konigthlem 9602 indpi 9941 nnsub 11271 2ndc1stc 21476 kgencn2 21582 tx1stc 21675 filuni 21910 fclscf 22050 alexsubALTlem2 22073 alexsubALTlem3 22074 alexsubALT 22076 lpni 27664 dfimafnf 29766 dfon2lem6 32019 nodenselem8 32168 finixpnum 33725 heiborlem4 33944 lncvrelatN 35588 imbi13 39246 dfaimafn 41769 sgoldbeven3prm 42199 |
Copyright terms: Public domain | W3C validator |