![]() |
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 247 ax12 2357 hbae 2365 tz7.7 6049 fvmptt 6608 f1oweALT 7478 wfrlem12 7763 nneneq 8488 pr2nelem 9216 cfcoflem 9484 nnunb 11696 ndvdssub 15610 lsmcv 19625 gsummoncoe1 20165 uvcendim 20683 2ndcsep 21761 atcvat4i 29945 mdsymlem5 29955 sumdmdii 29963 dfon2lem6 32493 colineardim1 32983 bj-hbaeb2 33572 hbae-o 35432 ax12fromc15 35434 cvrat4 35972 llncvrlpln2 36086 lplncvrlvol2 36144 dihmeetlem3N 37834 eel2122old 40415 |
Copyright terms: Public domain | W3C validator |