![]() |
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 396 |
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 206 df-an 397 |
This theorem is referenced by: ssnnfiOLD 9111 php4 9154 djulepw 10125 infdjuabs 10139 xrsupss 13225 xrinfmss 13226 trclfv 14882 isumsplit 15722 ram0 16891 0mhm 18627 grpidssd 18819 gexdvds 19362 lsmdisj2 19460 mulgnn0di 19600 odadd1 19622 gsumval3 19680 telgsums 19766 dprdfadd 19795 ringlz 20007 ringrz 20008 lspsneq 20579 dsmmacl 21143 mplsubglem 21401 scmatmhm 21879 mdetuni0 21966 mndifsplit 21981 chfacfscmulgsum 22205 chfacfpmmulgsum 22209 alexsublem 23391 ovolunlem1 24857 mbfi1fseqlem4 25079 deg1lt 25458 deg1invg 25467 sspz 29575 0lno 29630 pjhth 30233 pjhtheu 30234 pjpreeq 30238 opsqrlem1 30980 pfx1s2 31690 orng0le1 32002 0nellinds 32054 qqh1 32457 dnibndlem5 34934 relowlssretop 35823 mettrifi 36205 rngolz 36370 rngorz 36371 keridl 36480 lfl0f 37520 lkrlss 37546 lkrscss 37549 lkrin 37615 dihpN 39788 djh02 39865 lclkrlem1 39958 lclkr 39985 mon1pid 41508 mon1psubm 41509 minregex 41786 clsneiel1 42360 stoweidlem22 44233 stoweidlem34 44245 sqwvfoura 44439 elaa2lem 44444 nzrneg1ne0 46137 rnglz 46152 zrrnghm 46185 onsetreclem2 47121 |
Copyright terms: Public domain | W3C validator |