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 370 equvini 2346 equvel 2347 2eu6 2558 rgen2a 2977 rexraleqim 3328 elreldm 5350 tz6.12c 6213 onminex 7007 rntpos 7365 smores 7449 seqomlem2 7546 f1domg 7975 php 8144 fodomnum 8880 carduniima 8919 cardmin 9386 negn0 10459 sqrmo 13992 isch3 28098 cgrtriv 32109 wl-lem-moexsb 33350 grpomndo 33674 elghomlem2OLD 33685 |
Copyright terms: Public domain | W3C validator |