![]() |
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 1154 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an3.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: 3adant3l 1186 3adant3r 1188 syl3an3b 1473 syl3an3br 1476 disji 4873 ovmpt2x 7068 ovmpt2ga 7069 wfrlem14 7713 unbnn2 8507 axdc3lem4 9612 axdclem2 9679 gruiin 9969 gruen 9971 divass 11053 ltmul2 11230 xleadd1 12401 xltadd2 12403 xlemul1 12436 xltmul2 12439 elfzo 12795 modcyc2 13029 faclbnd5 13407 relexprel 14190 subcn2 14737 mulcn2 14738 ndvdsp1 15545 gcddiv 15678 lcmneg 15726 lubel 17512 gsumccatsn 17770 mulgaddcom 17954 oddvdsi 18355 odcong 18356 odeq 18357 efgsp1 18538 lspsnss 19389 lindsmm2 20576 mulmarep1el 20787 mdetunilem4 20830 iuncld 21261 neips 21329 opnneip 21335 comppfsc 21748 hmeof1o2 21979 ordthmeo 22018 ufinffr 22145 elfm3 22166 utop3cls 22467 blcntrps 22629 blcntr 22630 neibl 22718 blnei 22719 metss 22725 stdbdmetval 22731 prdsms 22748 blval2 22779 lmmbr 23468 lmmbr2 23469 iscau2 23487 bcthlem1 23534 bcthlem3 23536 bcthlem4 23537 dvn2bss 24134 dvfsumrlim 24235 dvfsumrlim2 24236 cxpexpz 24854 cxpsub 24869 cxpcom 24924 relogbzexp 24958 upgr4cycl4dv4e 27592 konigsbergssiedgwpr 27659 dlwwlknondlwlknonf1o 27795 dlwwlknondlwlknonf1oOLD 27796 hvaddsub12 28471 hvaddsubass 28474 hvsubdistr1 28482 hvsubcan 28507 hhssnv 28697 spanunsni 29014 homco1 29236 homulass 29237 hoadddir 29239 hosubdi 29243 hoaddsubass 29250 hosubsub4 29253 lnopmi 29435 adjlnop 29521 mdsymlem5 29842 disjif 29958 disjif2 29961 ind0 30682 sigaclfu 30784 bnj544 31567 bnj561 31576 bnj562 31577 bnj594 31585 clsint2 32916 ftc1anclem6 34120 isbnd2 34211 blbnd 34215 isdrngo2 34386 atnem0 35477 hlrelat5N 35560 ltrnel 36298 ltrnat 36299 ltrncnvat 36300 jm2.22 38531 jm2.23 38532 dvconstbi 39499 eelT11 39886 eelT12 39888 eelTT1 39889 eelT01 39890 eel0T1 39891 liminfvalxr 40933 rmfsupp 43180 mndpfsupp 43182 scmfsupp 43184 dignn0flhalflem2 43435 rrx2vlinest 43487 rrx2linesl 43489 |
Copyright terms: Public domain | W3C validator |