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 2422 hbae 2430 tz7.7 6339 fvmptt 6963 f1oweALT 7895 wfrlem12OLD 8233 nneneq 9086 nneneqOLD 9098 pr2nelemOLD 9872 cfcoflem 10141 nnunb 12342 ndvdssub 16225 lsmcv 20525 uvcendim 21176 gsummoncoe1 21597 2ndcsep 22732 atcvat4i 31137 mdsymlem5 31147 sumdmdii 31155 dfon2lem6 34153 colineardim1 34541 bj-hbaeb2 35178 hbae-o 37260 ax12fromc15 37262 cvrat4 37801 llncvrlpln2 37915 lplncvrlvol2 37973 dihmeetlem3N 39663 eel2122old 42764 |
Copyright terms: Public domain | W3C validator |