![]() |
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 1112 by Wolf Lammen, 20-Jun-2022.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3impa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1090 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3impa.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 206 df-3an 1090 |
This theorem is referenced by: 3imp 1112 3adant1 1131 3adant2 1132 ex3 1347 3impdir 1352 syl3an9b 1435 biimp3a 1470 stoic3 1779 rspec3 3264 rspc3v 3594 raltpg 4660 rextpg 4661 disjiun 5093 otthg 5443 3optocl 5729 fun2ssres 6547 funtpg 6557 funssfv 6864 f1elima 7211 ot1stg 7936 ot2ndg 7937 smogt 8314 omord2 8515 omword 8518 oeword 8538 omabslem 8597 ecovass 8764 fpmg 8807 findcard 9108 endjudisj 10105 cfsmolem 10207 ingru 10752 addasspi 10832 mulasspi 10834 ltapi 10840 ltmpi 10841 axpre-ltadd 11104 leltne 11245 dedekind 11319 recextlem2 11787 divdiv32 11864 divdiv1 11867 lble 12108 fnn0ind 12603 supminf 12861 xrleltne 13065 xrmaxeq 13099 xrmineq 13100 iccgelb 13321 elicc4 13332 iccsplit 13403 elfz 13431 modabs 13810 expgt0 14002 expge0 14005 expge1 14006 mulexpz 14009 expp1z 14018 expm1 14019 expmordi 14073 digit1 14141 faclbnd4 14198 faclbnd5 14199 ccatsymb 14471 s3eqs2s1eq 14828 abssubne0 15202 binom 15716 dvds0lem 16150 dvdsnegb 16157 muldvds1 16164 muldvds2 16165 dvdscmulr 16168 dvdsmulcr 16169 divalgmodcl 16290 gcd2n0cl 16390 gcdaddm 16406 lcmdvds 16485 prmdvdsexp 16592 rpexp1i 16600 monpropd 17621 prfval 18088 xpcpropd 18098 curf2ndf 18137 eqglact 18982 mndodcongi 19326 oddvdsnn0 19327 efgi0 19503 efgi1 19504 efgsval2 19516 lss0cl 20410 mpofrlmd 21186 scmatscmid 21858 pmatcollpw3fi1lem1 22138 cnpval 22590 cnf2 22603 cnnei 22636 lfinun 22879 ptpjcn 22965 cnmptk2 23040 flfval 23344 cnmpt2plusg 23442 cnmpt2vsca 23549 ustincl 23562 xbln0 23770 blssec 23791 blpnfctr 23792 mopni2 23852 mopni3 23853 nmoval 24082 nmocl 24087 isnghm2 24091 isnmhm2 24119 cnmpt2ds 24209 metdseq0 24220 cnmpt2ip 24615 caucfil 24650 mbfimasn 24999 dvnf 25294 dvnbss 25295 coemul 25616 dvply1 25647 dvnply2 25650 pserdvlem2 25790 logeftb 25942 advlogexp 26013 cxpne0 26035 cxpp1 26038 elno2 27005 f1otrg 27816 ax5seglem9 27889 uhgrn0 28021 upgrn0 28043 upgrle 28044 uhgrwkspthlem2 28705 frgrhash2wsp 29279 sspval 29668 sspnval 29682 lnof 29700 nmooval 29708 nmooge0 29712 nmoub3i 29718 bloln 29729 nmblore 29731 hosval 30685 homval 30686 hodval 30687 hfsval 30688 hfmval 30689 homulass 30747 hoadddir 30749 nmopub2tALT 30854 nmfnleub2 30871 kbval 30899 lnopmul 30912 0lnfn 30930 lnopcoi 30948 nmcoplb 30975 nmcfnlb 30999 kbass2 31062 nmopleid 31084 hstoh 31177 mdi 31240 dmdi 31247 dmdi4 31252 fdifsuppconst 31607 supxrnemnf 31676 reofld 32139 nsgmgclem 32192 ghmqusker 32201 rhmimaidl 32209 evls1fpws 32274 lbsdiflsp0 32324 zarclsun 32454 zarclsint 32456 bnj605 33522 bnj607 33531 bnj1097 33596 fnrelpredd 33696 cusgredgex 33718 topdifinffinlem 35821 lindsdom 36075 lindsenlbs 36076 ftc1anclem2 36155 fzmul 36203 nninfnub 36213 exidreslem 36339 grposnOLD 36344 ghomf 36352 rngohomf 36428 rngohom1 36430 rngohomadd 36431 rngohommul 36432 rngoiso1o 36441 rngoisohom 36442 igenmin 36526 lkrcl 37557 lkrf0 37558 omlfh1N 37723 tendoex 39441 uzindd 40437 sticksstones3 40559 sticksstones10 40566 sticksstones12a 40568 sticksstones12 40569 sticksstones17 40574 3anrabdioph 41108 3orrabdioph 41109 rencldnfilem 41146 dvdsabsmod0 41314 jm2.18 41315 jm2.25 41326 jm2.15nn0 41330 addrfv 42756 subrfv 42757 mulvfv 42758 bi3impa 42773 ssfiunibd 43550 supminfxr 43706 limsupgtlem 44025 xlimmnfv 44082 xlimpnfv 44086 dvnmul 44191 stoweidlem34 44282 stoweidlem48 44296 sge0cl 44629 sge0xp 44677 ovnsubaddlem1 44818 aovmpt4g 45440 gboge9 45963 |
Copyright terms: Public domain | W3C validator |