| 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 2428 hbae 2436 ceqsalt 3515 elabgt 3672 tz7.7 6410 fvmptt 7036 f1oweALT 7997 wfrlem12OLD 8360 nneneq 9246 nneneqOLD 9258 pr2nelemOLD 10043 cfcoflem 10312 nnunb 12522 ndvdssub 16446 lsmcv 21143 uvcendim 21867 gsummoncoe1 22312 2ndcsep 23467 atcvat4i 32416 mdsymlem5 32426 sumdmdii 32434 dfon2lem6 35789 colineardim1 36062 bj-hbaeb2 36819 hbae-o 38904 ax12fromc15 38906 cvrat4 39445 llncvrlpln2 39559 lplncvrlvol2 39617 dihmeetlem3N 41307 naddgeoa 43407 eel2122old 44738 |
| Copyright terms: Public domain | W3C validator |