Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl7 | Structured version Visualization version GIF version |
Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.) |
Ref | Expression |
---|---|
syl7.1 | ⊢ (𝜑 → 𝜓) |
syl7.2 | ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏))) |
Ref | Expression |
---|---|
syl7 | ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl7.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜒 → (𝜑 → 𝜓)) |
3 | syl7.2 | . 2 ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏))) | |
4 | 2, 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: syl7bi 258 ax12 2422 hbae 2430 tz7.7 6217 fvmptt 6816 f1oweALT 7723 wfrlem12 8044 nneneq 8807 pr2nelem 9583 cfcoflem 9851 nnunb 12051 ndvdssub 15933 lsmcv 20132 uvcendim 20763 gsummoncoe1 21179 2ndcsep 22310 atcvat4i 30432 mdsymlem5 30442 sumdmdii 30450 dfon2lem6 33434 colineardim1 34049 bj-hbaeb2 34687 hbae-o 36603 ax12fromc15 36605 cvrat4 37143 llncvrlpln2 37257 lplncvrlvol2 37315 dihmeetlem3N 39005 eel2122old 41952 |
Copyright terms: Public domain | W3C validator |