![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl3an3 | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
Ref | Expression |
---|---|
syl3an3.1 | ⊢ (𝜑 → 𝜃) |
syl3an3.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl3an3 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an3.1 | . . 3 ⊢ (𝜑 → 𝜃) | |
2 | 1 | 3anim3i 1151 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an3.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: 3adant3l 1177 3adant3r 1178 syl3an3b 1402 syl3an3br 1405 disji 5136 ovmpox 7579 ovmpoga 7580 wrecseq123 8329 wfrlem14OLD 8352 dif1en 9198 dif1enOLD 9200 domtrfil 9229 ssdomfi2 9234 domnsymfi 9237 sdomdomtrfi 9238 domsdomtrfi 9239 phplem2 9242 php 9244 php3 9246 findcard3 9319 unbnn2 9334 axdc3lem4 10496 axdclem2 10563 gruiin 10853 gruen 10855 divass 11941 ltmul2 12116 xleadd1 13288 xltadd2 13290 xlemul1 13323 xltmul2 13326 elfzo 13688 modcyc2 13927 faclbnd5 14315 relexprel 15044 subcn2 15597 mulcn2 15598 ndvdsp1 16413 gcddiv 16552 lcmneg 16604 lubel 18539 gsumccatsn 18833 mulgaddcom 19092 oddvdsi 19546 odcong 19547 odeq 19548 efgsp1 19735 lspsnss 20967 rnglidlrng 21236 lindsmm2 21827 mulmarep1el 22565 mdetunilem4 22608 iuncld 23040 neips 23108 opnneip 23114 comppfsc 23527 hmeof1o2 23758 ordthmeo 23797 ufinffr 23924 elfm3 23945 utop3cls 24247 blcntrps 24409 blcntr 24410 neibl 24501 blnei 24502 metss 24508 stdbdmetval 24514 prdsms 24531 blval2 24562 lmmbr 25277 lmmbr2 25278 iscau2 25296 bcthlem1 25343 bcthlem3 25345 bcthlem4 25346 dvn2bss 25951 dvfsumrlim 26057 dvfsumrlim2 26058 cxpexpz 26694 cxpsub 26709 cxpcom 26766 relogbzexp 26804 sltsub1 28083 1ewlk 30048 1pthon2ve 30087 upgr4cycl4dv4e 30118 konigsbergssiedgwpr 30182 dlwwlknondlwlknonf1o 30298 hvaddsub12 30971 hvaddsubass 30974 hvsubdistr1 30982 hvsubcan 31007 hhssnv 31197 spanunsni 31512 homco1 31734 homulass 31735 hoadddir 31737 hosubdi 31741 hoaddsubass 31748 hosubsub4 31751 lnopmi 31933 adjlnop 32019 mdsymlem5 32340 disjif 32498 disjif2 32501 ind0 33851 sigaclfu 33952 signstfvc 34420 bnj544 34739 bnj561 34748 bnj562 34749 bnj594 34757 swrdrevpfx 34944 satfvsuc 35189 satfvsucsuc 35193 clsint2 36041 ftc1anclem6 37399 isbnd2 37484 blbnd 37488 isdrngo2 37659 atnem0 39016 hlrelat5N 39100 ltrnel 39838 ltrnat 39839 ltrncnvat 39840 nnproddivdvdsd 41699 dvdsexpnn 42128 jm2.22 42653 jm2.23 42654 dvconstbi 44008 eelT11 44383 eelT12 44385 eelTT1 44386 eelT01 44387 eel0T1 44388 liminfvalxr 45404 rmfsupp 47753 mndpfsupp 47755 scmfsupp 47757 dignn0flhalflem2 48004 rrx2vlinest 48129 rrx2linesl 48131 |
Copyright terms: Public domain | W3C validator |