![]() |
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.) (Revised to shorten 3imp 1092 by Wolf Lammen, 20-Jun-2022.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3impa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1071 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3impa.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 209 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1069 |
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-3an 1071 |
This theorem is referenced by: 3imp 1092 3adant1 1111 3adant2 1112 ex3 1327 3impdir 1332 syl3an9b 1414 biimp3a 1449 stoic3 1740 rspec3 3164 rspc3v 3553 raltpg 4513 rextpg 4514 disjiun 4922 otthg 5238 3optocl 5501 fun2ssres 6237 funtpg 6247 funssfv 6525 f1elima 6852 ot1stg 7521 ot2ndg 7522 smogt 7814 omord2 8000 omword 8003 oeword 8023 omabslem 8079 ecovass 8210 fpmg 8238 findcard 8558 endjudisj 9398 cfsmolem 9496 ingru 10041 addasspi 10121 mulasspi 10123 ltapi 10129 ltmpi 10130 axpre-ltadd 10393 leltne 10536 dedekind 10609 recextlem2 11078 divdiv32 11155 divdiv1 11158 lble 11400 fnn0ind 11900 supminf 12155 xrleltne 12361 xrmaxeq 12395 xrmineq 12396 iccgelb 12615 elicc4 12625 iccsplit 12693 elfz 12720 modabs 13093 expgt0 13283 expge0 13286 expge1 13287 mulexpz 13290 expp1z 13299 expm1 13300 expmordi 13352 digit1 13419 faclbnd4 13478 faclbnd5 13479 s3eqs2s1eq 14168 abssubne0 14543 binom 15051 dvds0lem 15486 dvdsnegb 15493 muldvds1 15500 muldvds2 15501 dvdscmulr 15504 dvdsmulcr 15505 divalgmodcl 15624 gcd2n0cl 15724 gcdaddm 15739 lcmdvds 15814 prmdvdsexp 15921 rpexp1i 15927 monpropd 16877 prfval 17319 xpcpropd 17328 curf2ndf 17367 eqglact 18126 mndodcongi 18445 oddvdsnn0 18446 efgi0 18616 efgi1 18617 lss0cl 19452 mpofrlmd 20638 scmatscmid 20834 pmatcollpw3fi1lem1 21113 cnpval 21563 cnf2 21576 cnnei 21609 lfinun 21852 ptpjcn 21938 cnmptk2 22013 flfval 22317 cnmpt2plusg 22415 cnmpt2vsca 22521 ustincl 22534 xbln0 22742 blssec 22763 blpnfctr 22764 mopni2 22821 mopni3 22822 nmoval 23042 nmocl 23047 isnghm2 23051 isnmhm2 23079 cnmpt2ds 23169 metdseq0 23180 cnmpt2ip 23569 caucfil 23604 mbfimasn 23951 dvnf 24242 dvnbss 24243 coemul 24560 dvply1 24591 dvnply2 24594 pserdvlem2 24734 logeftb 24883 advlogexp 24954 cxpne0 24976 cxpp1 24979 f1otrg 26375 ax5seglem9 26441 uhgrn0 26570 upgrn0 26592 upgrle 26593 uhgrwkspthlem2 27258 frgrhash2wsp 27881 sspval 28292 sspnval 28306 lnof 28324 nmooval 28332 nmooge0 28336 nmoub3i 28342 bloln 28353 nmblore 28355 hosval 29313 homval 29314 hodval 29315 hfsval 29316 hfmval 29317 homulass 29375 hoadddir 29377 nmopub2tALT 29482 nmfnleub2 29499 kbval 29527 lnopmul 29540 0lnfn 29558 lnopcoi 29576 nmcoplb 29603 nmcfnlb 29627 kbass2 29690 nmopleid 29712 hstoh 29805 mdi 29868 dmdi 29875 dmdi4 29880 supxrnemnf 30269 reofld 30624 lbsdiflsp0 30683 bnj605 31858 bnj607 31867 bnj1097 31930 elno2 32722 topdifinffinlem 34110 lindsdom 34367 lindsenlbs 34368 ftc1anclem2 34449 fzmul 34498 nninfnub 34508 exidreslem 34637 grposnOLD 34642 ghomf 34650 rngohomf 34726 rngohom1 34728 rngohomadd 34729 rngohommul 34730 rngoiso1o 34739 rngoisohom 34740 igenmin 34824 lkrcl 35713 lkrf0 35714 omlfh1N 35879 tendoex 37596 3anrabdioph 38816 3orrabdioph 38817 rencldnfilem 38854 dvdsabsmod0 39021 jm2.18 39022 jm2.25 39033 jm2.15nn0 39037 addrfv 40260 subrfv 40261 mulvfv 40262 bi3impa 40277 ssfiunibd 41040 supminfxr 41206 limsupgtlem 41524 xlimmnfv 41581 xlimpnfv 41585 dvnmul 41693 stoweidlem34 41785 stoweidlem48 41799 sge0cl 42129 sge0xp 42177 ovnsubaddlem1 42318 aovmpt4g 42841 gboge9 43332 |
Copyright terms: Public domain | W3C validator |