Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3impa | Structured version Visualization version GIF version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3impa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impa.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
2 | 1 | exp31 628 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1249 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ 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: ex3 1255 3impdir 1374 syl3an9b 1389 biimp3a 1424 stoic3 1692 rspec3 2919 rspc3v 3296 raltpg 4183 rextpg 4184 disjiun 4573 otthg 4880 3optocl 5120 fun2ssres 5845 funtpg 5856 funssfv 6119 foco2OLD 6288 f1elima 6421 ot1stg 7073 ot2ndg 7074 smogt 7351 omord2 7534 omword 7537 oeword 7557 omabslem 7613 ecovass 7742 fpmg 7769 findcard 8084 cdaun 8877 cfsmolem 8975 ingru 9516 addasspi 9596 mulasspi 9598 ltapi 9604 ltmpi 9605 axpre-ltadd 9867 leltne 10006 dedekind 10079 recextlem2 10537 divdiv32 10612 divdiv1 10615 lble 10854 fnn0ind 11352 supminf 11651 xrleltne 11854 xrmaxeq 11884 xrmineq 11885 iccgelb 12101 elicc4 12111 iccsplit 12176 elfz 12203 fzrevral 12294 modabs 12565 expgt0 12755 expge0 12758 expge1 12759 mulexpz 12762 expp1z 12771 expm1 12772 digit1 12860 faclbnd4 12946 faclbnd5 12947 abssubne0 13904 binom 14401 dvds0lem 14830 dvdsnegb 14837 muldvds1 14844 muldvds2 14845 dvdscmulr 14848 dvdsmulcr 14849 divalgmodcl 14969 gcd2n0cl 15069 gcdaddm 15084 lcmdvds 15159 prmdvdsexp 15265 rpexp1i 15271 monpropd 16220 prfval 16662 xpcpropd 16671 curf2ndf 16710 eqglact 17468 mndodcongi 17785 oddvdsnn0 17786 efgi0 17956 efgi1 17957 lss0cl 18768 scmatscmid 20131 pmatcollpw3fi1lem1 20410 cnpval 20850 cnf2 20863 cnnei 20896 lfinun 21138 ptpjcn 21224 cnmptk2 21299 flfval 21604 cnmpt2plusg 21702 cnmpt2vsca 21808 ustincl 21821 xbln0 22029 blssec 22050 blpnfctr 22051 mopni2 22108 mopni3 22109 nmoval 22329 nmocl 22334 isnghm2 22338 isnmhm2 22366 cnmpt2ds 22454 metdseq0 22465 cnmpt2ip 22855 caucfil 22889 mbfimasn 23207 dvnf 23496 dvnbss 23497 coemul 23812 dvply1 23843 dvnply2 23846 pserdvlem2 23986 logeftb 24134 advlogexp 24201 cxpne0 24223 cxpp1 24226 lgsne0 24860 f1otrg 25551 ax5seglem9 25617 uhgrn0 25733 upgrn0 25756 upgrle 25757 umgrass 25848 umgran0 25849 umgrale 25850 nbgraf1olem3 25972 pthdepisspth 26104 sspval 26962 sspnval 26976 lnof 26994 nmooval 27002 nmooge0 27006 nmoub3i 27012 bloln 27023 nmblore 27025 hosval 27983 homval 27984 hodval 27985 hfsval 27986 hfmval 27987 homulass 28045 hoadddir 28047 nmopub2tALT 28152 nmfnleub2 28169 kbval 28197 lnopmul 28210 0lnfn 28228 lnopcoi 28246 nmcoplb 28273 nmcfnlb 28297 kbass2 28360 nmopleid 28382 hstoh 28475 mdi 28538 dmdi 28545 dmdi4 28550 supxrnemnf 28924 reofld 29171 bnj605 30231 bnj607 30240 bnj1097 30303 elno2 31051 topdifinffinlem 32371 lindsdom 32573 lindsenlbs 32574 ftc1anclem2 32656 fzmul 32707 nninfnub 32717 exidreslem 32846 grposnOLD 32851 ghomf 32859 rngohomf 32935 rngohom1 32937 rngohomadd 32938 rngohommul 32939 rngoiso1o 32948 rngoisohom 32949 igenmin 33033 lkrcl 33397 lkrf0 33398 omlfh1N 33563 tendoex 35281 3anrabdioph 36364 3orrabdioph 36365 rencldnfilem 36402 expmordi 36530 dvdsabsmod0 36572 jm2.18 36573 jm2.25 36584 jm2.15nn0 36588 addrfv 37694 subrfv 37695 mulvfv 37696 bi3impa 37711 ssfiunibd 38464 dvnmul 38833 stoweidlem34 38927 stoweidlem48 38941 sge0cl 39274 sge0xp 39322 ovnsubaddlem1 39460 ovnovollem3 39548 aovmpt4g 39930 gboage9 40186 uhgr1wlkspthlem2 40960 |
Copyright terms: Public domain | W3C validator |