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 75 | . 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 688 ax12v2 2036 ax12vOLD 2037 ax12vOLDOLD 2038 nfimdOLD 2214 fununi 5878 dfimafn 6155 funimass3 6241 isomin 6487 oneqmin 6897 tz7.48lem 7423 fisupg 8093 fiinfg 8288 trcl 8487 coflim 8966 coftr 8978 axdc3lem2 9156 konigthlem 9269 indpi 9608 nnsub 10936 2ndc1stc 21064 kgencn2 21170 tx1stc 21263 filuni 21499 fclscf 21639 alexsubALTlem2 21662 alexsubALTlem3 21663 alexsubALT 21665 lpni 26722 dfimafnf 28817 dfon2lem6 30937 nodenselem8 31087 finixpnum 32564 heiborlem4 32783 lncvrelatN 34085 imbi13 37747 dfaimafn 39894 |
Copyright terms: Public domain | W3C validator |