![]() |
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 ceqsalt 3506 tz7.7 6391 fvmptt 7019 f1oweALT 7959 wfrlem12OLD 8320 nneneq 9209 nneneqOLD 9221 pr2nelemOLD 9998 cfcoflem 10267 nnunb 12468 ndvdssub 16352 lsmcv 20754 uvcendim 21402 gsummoncoe1 21828 2ndcsep 22963 atcvat4i 31650 mdsymlem5 31660 sumdmdii 31668 dfon2lem6 34760 colineardim1 35033 bj-hbaeb2 35696 hbae-o 37773 ax12fromc15 37775 cvrat4 38314 llncvrlpln2 38428 lplncvrlvol2 38486 dihmeetlem3N 40176 naddgeoa 42145 eel2122old 43479 |
Copyright terms: Public domain | W3C validator |