![]() |
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 585 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: ssnnfiOLD 9120 php4 9163 djulepw 10136 infdjuabs 10150 xrsupss 13237 xrinfmss 13238 trclfv 14894 isumsplit 15733 ram0 16902 0mhm 18638 grpidssd 18831 gexdvds 19374 lsmdisj2 19472 mulgnn0di 19612 odadd1 19634 gsumval3 19692 telgsums 19778 dprdfadd 19807 ringlz 20019 ringrz 20020 lspsneq 20628 dsmmacl 21170 mplsubglem 21428 scmatmhm 21906 mdetuni0 21993 mndifsplit 22008 chfacfscmulgsum 22232 chfacfpmmulgsum 22236 alexsublem 23418 ovolunlem1 24884 mbfi1fseqlem4 25106 deg1lt 25485 deg1invg 25494 sspz 29726 0lno 29781 pjhth 30384 pjhtheu 30385 pjpreeq 30389 opsqrlem1 31131 pfx1s2 31851 orng0le1 32161 0nellinds 32213 qqh1 32630 dnibndlem5 34998 relowlssretop 35884 mettrifi 36266 rngolz 36431 rngorz 36432 keridl 36541 lfl0f 37581 lkrlss 37607 lkrscss 37610 lkrin 37676 dihpN 39849 djh02 39926 lclkrlem1 40019 lclkr 40046 mon1pid 41579 mon1psubm 41580 minregex 41898 clsneiel1 42472 stoweidlem22 44353 stoweidlem34 44365 sqwvfoura 44559 elaa2lem 44564 nzrneg1ne0 46257 rnglz 46272 zrrnghm 46305 onsetreclem2 47241 |
Copyright terms: Public domain | W3C validator |