![]() |
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.) |
Ref | Expression |
---|---|
syl3an3.1 | ⊢ (𝜑 → 𝜃) |
syl3an3.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl3an3 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an3.1 | . . 3 ⊢ (𝜑 → 𝜃) | |
2 | syl3an3.2 | . . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
3 | 2 | 3exp 1256 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syl7 72 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏))) |
5 | 4 | 3imp 1249 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: syl3an3b 1356 syl3an3br 1359 vtoclgftOLD 3228 disji 4570 ovmpt2x 6687 ovmpt2ga 6688 wfrlem14 7315 unbnn2 8102 axdc3lem4 9158 axdclem2 9225 gruiin 9511 gruen 9513 divass 10582 ltmul2 10753 xleadd1 11957 xltadd2 11959 xlemul1 11992 xltmul2 11995 elfzo 12341 modcyc2 12568 faclbnd5 12947 relexprel 13627 subcn2 14173 mulcn2 14174 ndvdsp1 14973 gcddiv 15106 lcmneg 15154 lubel 16945 gsumccatsn 17203 mulgaddcom 17387 oddvdsi 17790 odcong 17791 odeq 17792 efgsp1 17973 lspsnss 18811 lindsmm2 19987 mulmarep1el 20197 mdetunilem4 20240 iuncld 20659 neips 20727 opnneip 20733 comppfsc 21145 hmeof1o2 21376 ordthmeo 21415 ufinffr 21543 elfm3 21564 utop3cls 21865 blcntrps 22027 blcntr 22028 neibl 22116 blnei 22117 metss 22123 stdbdmetval 22129 prdsms 22146 blval2 22177 lmmbr 22864 lmmbr2 22865 iscau2 22883 bcthlem1 22929 bcthlem3 22931 bcthlem4 22932 dvn2bss 23499 dvfsumrlim 23598 dvfsumrlim2 23599 cxpexpz 24213 cxpsub 24228 relogbzexp 24314 wlkcompim 26054 wwlknext 26252 wwlkextproplem3 26271 clwlkcompim 26292 clwwlkel 26321 clwwlkf 26322 numclwlk1lem2f1 26621 hvaddsub12 27279 hvaddsubass 27282 hvsubdistr1 27290 hvsubcan 27315 hhssnv 27505 spanunsni 27822 homco1 28044 homulass 28045 hoadddir 28047 hosubdi 28051 hoaddsubass 28058 hosubsub4 28061 lnopmi 28243 adjlnop 28329 mdsymlem5 28650 disjif 28773 disjif2 28776 ind0 29409 sigaclfu 29509 bnj544 30218 bnj561 30227 bnj562 30228 bnj594 30236 clsint2 31494 ftc1anclem6 32660 isbnd2 32752 blbnd 32756 isdrngo2 32927 atnem0 33623 hlrelat5N 33705 ltrnel 34443 ltrnat 34444 ltrncnvat 34445 jm2.22 36580 jm2.23 36581 dvconstbi 37555 eelT11 37953 eelT12 37955 eelTT1 37956 eelT01 37957 eel0T1 37958 upgr4cycl4dv4e 41352 konigsbergssiedgwpr 41418 rmfsupp 41949 mndpfsupp 41951 scmfsupp 41953 dignn0flhalflem2 42208 |
Copyright terms: Public domain | W3C validator |