| 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 1155 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
| 3 | syl3an3.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
| 4 | 2, 3 | syl 17 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ 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: 3adant3l 1181 3adant3r 1182 syl3an3b 1407 syl3an3br 1410 disji 5128 ovmpox 7586 ovmpoga 7587 wrecseq123 8339 wfrlem14OLD 8362 dif1en 9200 dif1enOLD 9202 domtrfil 9232 ssdomfi2 9237 domnsymfi 9240 sdomdomtrfi 9241 domsdomtrfi 9242 phplem2 9245 php 9247 php3 9249 findcard3 9318 unbnn2 9333 axdc3lem4 10493 axdclem2 10560 gruiin 10850 gruen 10852 divass 11940 ltmul2 12118 xleadd1 13297 xltadd2 13299 xlemul1 13332 xltmul2 13335 elfzo 13701 modcyc2 13947 faclbnd5 14337 relexprel 15078 subcn2 15631 mulcn2 15632 ndvdsp1 16448 gcddiv 16588 lcmneg 16640 lubel 18559 mndpfsupp 18780 gsumccatsn 18856 mulgaddcom 19116 oddvdsi 19566 odcong 19567 odeq 19568 efgsp1 19755 lspsnss 20988 rnglidlrng 21257 lindsmm2 21849 mulmarep1el 22578 mdetunilem4 22621 iuncld 23053 neips 23121 opnneip 23127 comppfsc 23540 hmeof1o2 23771 ordthmeo 23810 ufinffr 23937 elfm3 23958 utop3cls 24260 blcntrps 24422 blcntr 24423 neibl 24514 blnei 24515 metss 24521 stdbdmetval 24527 prdsms 24544 blval2 24575 lmmbr 25292 lmmbr2 25293 iscau2 25311 bcthlem1 25358 bcthlem3 25360 bcthlem4 25361 dvn2bss 25966 dvfsumrlim 26072 dvfsumrlim2 26073 cxpexpz 26709 cxpsub 26724 cxpcom 26781 relogbzexp 26819 sltsub1 28106 1ewlk 30134 1pthon2ve 30173 upgr4cycl4dv4e 30204 konigsbergssiedgwpr 30268 dlwwlknondlwlknonf1o 30384 hvaddsub12 31057 hvaddsubass 31060 hvsubdistr1 31068 hvsubcan 31093 hhssnv 31283 spanunsni 31598 homco1 31820 homulass 31821 hoadddir 31823 hosubdi 31827 hoaddsubass 31834 hosubsub4 31837 lnopmi 32019 adjlnop 32105 mdsymlem5 32426 disjif 32591 disjif2 32594 ind0 32843 sigaclfu 34120 signstfvc 34589 bnj544 34908 bnj561 34917 bnj562 34918 bnj594 34926 swrdrevpfx 35122 satfvsuc 35366 satfvsucsuc 35370 clsint2 36330 weiunso 36467 weiunwe 36470 ftc1anclem6 37705 isbnd2 37790 blbnd 37794 isdrngo2 37965 atnem0 39319 hlrelat5N 39403 ltrnel 40141 ltrnat 40142 ltrncnvat 40143 nnproddivdvdsd 42001 dvdsexpnn 42368 jm2.22 43007 jm2.23 43008 dvconstbi 44353 eelT11 44727 eelT12 44729 eelTT1 44730 eelT01 44731 eel0T1 44732 liminfvalxr 45798 rmfsupp 48289 scmfsupp 48291 dignn0flhalflem2 48537 rrx2vlinest 48662 rrx2linesl 48664 |
| Copyright terms: Public domain | W3C validator |