![]() |
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 254 ax12 2417 hbae 2425 ceqsalt 3496 elabgt 3658 tz7.7 6394 fvmptt 7021 f1oweALT 7978 wfrlem12OLD 8342 nneneq 9236 nneneqOLD 9248 pr2nelemOLD 10039 cfcoflem 10306 nnunb 12514 ndvdssub 16406 lsmcv 21118 uvcendim 21841 gsummoncoe1 22296 2ndcsep 23451 atcvat4i 32327 mdsymlem5 32337 sumdmdii 32345 dfon2lem6 35625 colineardim1 35898 bj-hbaeb2 36536 hbae-o 38614 ax12fromc15 38616 cvrat4 39155 llncvrlpln2 39269 lplncvrlvol2 39327 dihmeetlem3N 41017 naddgeoa 43098 eel2122old 44431 |
Copyright terms: Public domain | W3C validator |