![]() |
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 245 syl3an3 1498 ax12 2437 hbae 2445 ax12OLD 2469 tz7.7 5898 fvmptt 6450 f1oweALT 7305 wfrlem12 7583 nneneq 8296 pr2nelem 8988 cfcoflem 9257 nnunb 11451 ndvdssub 15306 lsmcv 19314 gsummoncoe1 19847 uvcendim 20359 2ndcsep 21435 atcvat4i 29536 mdsymlem5 29546 sumdmdii 29554 dfon2lem6 31969 colineardim1 32445 bj-hbaeb2 33082 hbae-o 34661 ax12fromc15 34663 cvrat4 35201 llncvrlpln2 35315 lplncvrlvol2 35373 dihmeetlem3N 37065 eel2122old 39414 |
Copyright terms: Public domain | W3C validator |