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 255 ax12 2423 hbae 2431 tz7.7 6340 fvmptt 6964 f1oweALT 7896 wfrlem12OLD 8234 nneneq 9087 nneneqOLD 9099 pr2nelemOLD 9873 cfcoflem 10142 nnunb 12343 ndvdssub 16226 lsmcv 20525 uvcendim 21176 gsummoncoe1 21597 2ndcsep 22732 atcvat4i 31125 mdsymlem5 31135 sumdmdii 31143 dfon2lem6 34141 colineardim1 34532 bj-hbaeb2 35169 hbae-o 37251 ax12fromc15 37253 cvrat4 37792 llncvrlpln2 37906 lplncvrlvol2 37964 dihmeetlem3N 39654 eel2122old 42733 |
Copyright terms: Public domain | W3C validator |