![]() |
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 261 bija 373 equviniOLD 2393 equvel 2394 2eu6 2690 rgen2a 3171 rexraleqim 3550 elreldm 5646 tz6.12c 6522 onminex 7337 rntpos 7707 smores 7792 seqomlem2 7889 f1domg 8325 php 8496 fodomnum 9276 carduniima 9315 cardmin 9783 negn0 10869 sqrmo 14471 isch3 28813 cgrtriv 33017 wl-lem-moexsb 34278 grpomndo 34628 elghomlem2OLD 34639 tz6.12c-afv2 42877 |
Copyright terms: Public domain | W3C validator |