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 257 bija 369 equvini 2334 equvel 2335 2eu6 2546 rgen2a 2960 rexraleqim 3299 elreldm 5271 tz6.12c 6123 onminex 6899 rntpos 7252 smores 7336 seqomlem2 7433 f1domg 7861 php 8029 fodomnum 8763 carduniima 8802 cardmin 9265 negn0 10338 sqrmo 13840 isch3 27482 cgrtriv 31279 wl-lem-moexsb 32529 grpomndo 32844 elghomlem2OLD 32855 |
Copyright terms: Public domain | W3C validator |