![]() |
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 268 bija 379 equvel 2449 2eu6 2645 rgen2a 3354 rexraleqim 3630 elreldm 5937 tz6.12cOLD 6923 onminex 7806 rntpos 8245 smores 8373 seqomlem2 8472 f1domg 8993 php 9238 phpOLD 9250 fodomnum 10087 carduniima 10126 cardmin 10594 negn0 11680 sqrmo 15242 isch3 31143 cgrtriv 35749 wl-lem-moexsb 37186 grpomndo 37499 elghomlem2OLD 37510 tz6.12c-afv2 46765 |
Copyright terms: Public domain | W3C validator |