![]() |
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 1158 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an3.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: 3adant3l 1194 3adant3r 1196 syl3an3b 1512 syl3an3br 1515 vtoclgftOLD 3391 disji 4785 ovmpt2x 6950 ovmpt2ga 6951 wfrlem14 7593 unbnn2 8378 axdc3lem4 9463 axdclem2 9530 gruiin 9820 gruen 9822 divass 10891 ltmul2 11062 xleadd1 12274 xltadd2 12276 xlemul1 12309 xltmul2 12312 elfzo 12662 modcyc2 12896 faclbnd5 13275 relexprel 13974 subcn2 14520 mulcn2 14521 ndvdsp1 15333 gcddiv 15466 lcmneg 15514 lubel 17319 gsumccatsn 17577 mulgaddcom 17761 oddvdsi 18163 odcong 18164 odeq 18165 efgsp1 18346 lspsnss 19188 lindsmm2 20366 mulmarep1el 20576 mdetunilem4 20619 iuncld 21047 neips 21115 opnneip 21121 comppfsc 21533 hmeof1o2 21764 ordthmeo 21803 ufinffr 21930 elfm3 21951 utop3cls 22252 blcntrps 22414 blcntr 22415 neibl 22503 blnei 22504 metss 22510 stdbdmetval 22516 prdsms 22533 blval2 22564 lmmbr 23252 lmmbr2 23253 iscau2 23271 bcthlem1 23317 bcthlem3 23319 bcthlem4 23320 dvn2bss 23888 dvfsumrlim 23989 dvfsumrlim2 23990 cxpexpz 24608 cxpsub 24623 relogbzexp 24709 upgr4cycl4dv4e 27333 konigsbergssiedgwpr 27397 dlwwlknondlwlknonf1o 27522 hvaddsub12 28200 hvaddsubass 28203 hvsubdistr1 28211 hvsubcan 28236 hhssnv 28426 spanunsni 28743 homco1 28965 homulass 28966 hoadddir 28968 hosubdi 28972 hoaddsubass 28979 hosubsub4 28982 lnopmi 29164 adjlnop 29250 mdsymlem5 29571 disjif 29694 disjif2 29697 ind0 30385 sigaclfu 30487 bnj544 31267 bnj561 31276 bnj562 31277 bnj594 31285 clsint2 32626 ftc1anclem6 33799 isbnd2 33891 blbnd 33895 isdrngo2 34066 atnem0 35104 hlrelat5N 35186 ltrnel 35924 ltrnat 35925 ltrncnvat 35926 jm2.22 38060 jm2.23 38061 dvconstbi 39031 eelT11 39430 eelT12 39432 eelTT1 39433 eelT01 39434 eel0T1 39435 liminfvalxr 40514 rmfsupp 42661 mndpfsupp 42663 scmfsupp 42665 dignn0flhalflem2 42916 |
Copyright terms: Public domain | W3C validator |