![]() |
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 258 bija 369 equvini 2492 equvel 2493 2eu6 2707 rgen2a 3126 rexraleqim 3478 elreldm 5486 tz6.12c 6352 onminex 7152 rntpos 7515 smores 7600 seqomlem2 7697 f1domg 8127 php 8298 fodomnum 9078 carduniima 9117 cardmin 9586 negn0 10659 sqrmo 14193 isch3 28431 cgrtriv 32439 wl-lem-moexsb 33677 grpomndo 33999 elghomlem2OLD 34010 |
Copyright terms: Public domain | W3C validator |