![]() |
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 |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl221anc.6 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl221anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | 3, 4 | jca 512 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl221anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) | |
8 | 1, 2, 5, 6, 7 | syl211anc 1369 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: syl222anc 1379 vtocldf 3498 f1oprswap 6526 dmdcand 11293 modmul12d 13143 modnegd 13144 modadd12d 13145 exprec 13320 rpexpmord 13382 splval2 13955 dvdsmodexp 15448 eulerthlem2 15948 fermltl 15950 odzdvds 15961 fnpr2o 16659 efgredleme 18596 efgredlemc 18598 blssps 22717 blss 22718 metequiv2 22803 met1stc 22814 met2ndci 22815 metdstri 23142 xlebnum 23252 caubl 23594 divcxp 24951 cxple2a 24963 cxplead 24985 cxplt2d 24990 cxple2d 24991 mulcxpd 24992 ang180 25073 wilthlem2 25328 lgsvalmod 25574 lgsmod 25581 lgsdir2lem4 25586 lgsdirprm 25589 lgsne0 25593 lgseisen 25637 ax5seglem9 26406 xrsmulgzz 30339 linds2eq 30587 conway 32873 etasslt 32883 heiborlem8 34628 cdlemd4 36868 cdleme15a 36941 cdleme17b 36954 cdleme25a 37020 cdleme25c 37022 cdleme25dN 37023 cdleme26ee 37027 tendococl 37439 tendodi1 37451 tendodi2 37452 cdlemi 37487 tendocan 37491 cdlemk5a 37502 cdlemk5 37503 cdlemk10 37510 cdlemk5u 37528 cdlemkfid1N 37588 pellexlem6 38916 acongeq 39065 jm2.25 39081 stoweidlem42 41869 stoweidlem51 41878 ldepspr 44008 |
Copyright terms: Public domain | W3C validator |