|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > syl2anc2 | Structured version Visualization version GIF version | ||
| Description: Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.) | 
| Ref | Expression | 
|---|---|
| syl2anc2.1 | ⊢ (𝜑 → 𝜓) | 
| syl2anc2.2 | ⊢ (𝜓 → 𝜒) | 
| syl2anc2.3 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | 
| Ref | Expression | 
|---|---|
| syl2anc2 | ⊢ (𝜑 → 𝜃) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | syl2anc2.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | syl2anc2.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) | 
| 4 | syl2anc2.3 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
| 5 | 1, 3, 4 | syl2anc 584 | 1 ⊢ (𝜑 → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 | 
| This theorem is referenced by: php4 9250 djulepw 10233 infdjuabs 10245 xrsupss 13351 xrinfmss 13352 trclfv 15039 isumsplit 15876 ram0 17060 0mhm 18832 grpidssd 19034 gexdvds 19602 lsmdisj2 19700 mulgnn0di 19843 odadd1 19866 gsumval3 19925 telgsums 20011 dprdfadd 20040 rnglz 20162 rngrz 20163 zrrnghm 20536 lspsneq 21124 rnglidl0 21239 rngqiprngimf1 21310 rngqiprngfulem5 21325 dsmmacl 21761 mplsubglem 22019 scmatmhm 22540 mdetuni0 22627 mndifsplit 22642 chfacfscmulgsum 22866 chfacfpmmulgsum 22870 alexsublem 24052 ovolunlem1 25532 mbfi1fseqlem4 25753 deg1lt 26136 deg1invg 26145 mon1pid 26193 sspz 30754 0lno 30809 pjhth 31412 pjhtheu 31413 pjpreeq 31417 opsqrlem1 32159 pfx1s2 32923 gsumwun 33068 orng0le1 33342 0nellinds 33398 irredminply 33757 qqh1 33986 dnibndlem5 36483 relowlssretop 37364 mettrifi 37764 rngolz 37929 rngorz 37930 keridl 38039 lfl0f 39070 lkrlss 39096 lkrscss 39099 lkrin 39165 dihpN 41338 djh02 41415 lclkrlem1 41508 lclkr 41535 mon1psubm 43211 minregex 43547 clsneiel1 44121 stoweidlem22 46037 stoweidlem34 46049 sqwvfoura 46243 elaa2lem 46248 nzrneg1ne0 48146 onsetreclem2 49225 | 
| Copyright terms: Public domain | W3C validator |