|   | 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 511 | . 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏)) | 
| 6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
| 7 | syl221anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) | |
| 8 | 1, 2, 5, 6, 7 | syl211anc 1378 | 1 ⊢ (𝜑 → 𝜁) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 | 
| 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 207 df-an 396 df-3an 1089 | 
| This theorem is referenced by: syl222anc 1388 vtocldf 3560 f1oprswap 6892 dmdcand 12072 modmul12d 13966 modnegd 13967 modadd12d 13968 exprec 14144 rpexpmord 14208 splval2 14795 dvdsmodexp 16298 eulerthlem2 16819 fermltl 16821 odzdvds 16833 fnpr2o 17602 efgredleme 19761 efgredlemc 19763 blssps 24434 blss 24435 metequiv2 24523 met1stc 24534 met2ndci 24535 metdstri 24873 xlebnum 24997 caubl 25342 divcxp 26729 cxple2a 26741 cxplead 26763 cxplt2d 26768 cxple2d 26769 mulcxpd 26770 ang180 26857 wilthlem2 27112 lgsvalmod 27360 lgsmod 27367 lgsdir2lem4 27372 lgsdirprm 27375 lgsne0 27379 lgseisen 27423 conway 27844 ax5seglem9 28952 fzm1ne1 32790 xrsmulgzz 33011 linds2eq 33409 heiborlem8 37825 cdlemd4 40203 cdleme15a 40276 cdleme17b 40289 cdleme25a 40355 cdleme25c 40357 cdleme25dN 40358 cdleme26ee 40362 tendococl 40774 tendodi1 40786 tendodi2 40787 cdlemi 40822 tendocan 40826 cdlemk5a 40837 cdlemk5 40838 cdlemk10 40845 cdlemk5u 40863 cdlemkfid1N 40923 pellexlem6 42845 acongeq 42995 jm2.25 43011 stoweidlem42 46057 stoweidlem51 46066 ldepspr 48390 | 
| Copyright terms: Public domain | W3C validator |