![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl221anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl221anc.6 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl221anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | 3, 4 | jca 497 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl221anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) | |
8 | 1, 2, 5, 6, 7 | syl211anc 1482 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 383 df-3an 1073 |
This theorem is referenced by: syl222anc 1492 vtocldf 3408 f1oprswap 6322 dmdcand 11033 modmul12d 12933 modnegd 12934 modadd12d 12935 exprec 13109 splval2 13718 dvdsmodexp 15198 eulerthlem2 15695 fermltl 15697 odzdvds 15708 efgredleme 18364 efgredlemc 18366 blssps 22450 blss 22451 metequiv2 22536 met1stc 22547 met2ndci 22548 metdstri 22875 xlebnum 22985 caubl 23326 divcxp 24655 cxple2a 24667 cxplead 24689 cxplt2d 24694 cxple2d 24695 mulcxpd 24696 ang180 24766 wilthlem2 25017 lgsvalmod 25263 lgsmod 25270 lgsdir2lem4 25275 lgsdirprm 25278 lgsne0 25282 lgseisen 25326 ax5seglem9 26039 xrsmulgzz 30019 conway 32248 etasslt 32258 heiborlem8 33950 cdlemd4 36011 cdleme15a 36084 cdleme17b 36097 cdleme25a 36163 cdleme25c 36165 cdleme25dN 36166 cdleme26ee 36170 tendococl 36582 tendodi1 36594 tendodi2 36595 cdlemi 36630 tendocan 36634 cdlemk5a 36645 cdlemk5 36646 cdlemk10 36653 cdlemk5u 36671 cdlemkfid1N 36731 pellexlem6 37925 rpexpmord 38040 acongeq 38077 jm2.25 38093 stoweidlem42 40777 stoweidlem51 40786 ldepspr 42791 |
Copyright terms: Public domain | W3C validator |