| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syli | Structured version Visualization version GIF version | ||
| Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.) |
| Ref | Expression |
|---|---|
| syli.1 | ⊢ (𝜓 → (𝜑 → 𝜒)) |
| syli.2 | ⊢ (𝜒 → (𝜑 → 𝜃)) |
| Ref | Expression |
|---|---|
| syli | ⊢ (𝜓 → (𝜑 → 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syli.1 | . 2 ⊢ (𝜓 → (𝜑 → 𝜒)) | |
| 2 | syli.2 | . . 3 ⊢ (𝜒 → (𝜑 → 𝜃)) | |
| 3 | 2 | com12 32 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
| 4 | 1, 3 | sylcom 30 | 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: ibd 269 bija 380 equvel 2461 2eu6 2657 rgen2a 3371 rexraleqim 3647 elreldm 5946 tz6.12cOLD 6933 onminex 7822 rntpos 8264 smores 8392 seqomlem2 8491 f1domg 9012 php 9247 phpOLD 9259 fodomnum 10097 carduniima 10136 cardmin 10604 negn0 11692 sqrmo 15290 isch3 31260 cgrtriv 36003 wl-lem-moexsb 37569 grpomndo 37882 elghomlem2OLD 37893 tz6.12c-afv2 47254 |
| Copyright terms: Public domain | W3C validator |