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 1103 by Wolf Lammen, 20-Jun-2022.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3impa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1081 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3impa.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 218 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-3an 1081 |
This theorem is referenced by: 3imp 1103 3adant1 1122 3adant2 1123 ex3 1338 3impdir 1343 syl3an9b 1425 biimp3a 1460 stoic3 1768 rspec3 3209 rspc3v 3633 raltpg 4626 rextpg 4627 disjiun 5044 otthg 5368 3optocl 5640 fun2ssres 6392 funtpg 6402 funssfv 6684 f1elima 7012 ot1stg 7692 ot2ndg 7693 smogt 7993 omord2 8182 omword 8185 oeword 8205 omabslem 8262 ecovass 8393 fpmg 8421 findcard 8745 endjudisj 9582 cfsmolem 9680 ingru 10225 addasspi 10305 mulasspi 10307 ltapi 10313 ltmpi 10314 axpre-ltadd 10577 leltne 10718 dedekind 10791 recextlem2 11259 divdiv32 11336 divdiv1 11339 lble 11581 fnn0ind 12069 supminf 12323 xrleltne 12526 xrmaxeq 12560 xrmineq 12561 iccgelb 12781 elicc4 12791 iccsplit 12859 elfz 12886 modabs 13260 expgt0 13450 expge0 13453 expge1 13454 mulexpz 13457 expp1z 13466 expm1 13467 expmordi 13519 digit1 13586 faclbnd4 13645 faclbnd5 13646 ccatsymb 13924 s3eqs2s1eq 14288 abssubne0 14664 binom 15173 dvds0lem 15608 dvdsnegb 15615 muldvds1 15622 muldvds2 15623 dvdscmulr 15626 dvdsmulcr 15627 divalgmodcl 15746 gcd2n0cl 15846 gcdaddm 15861 lcmdvds 15940 prmdvdsexp 16047 rpexp1i 16053 monpropd 16995 prfval 17437 xpcpropd 17446 curf2ndf 17485 eqglact 18269 mndodcongi 18600 oddvdsnn0 18601 efgi0 18775 efgi1 18776 efgsval2 18788 lss0cl 19647 mpofrlmd 20849 scmatscmid 21043 pmatcollpw3fi1lem1 21322 cnpval 21772 cnf2 21785 cnnei 21818 lfinun 22061 ptpjcn 22147 cnmptk2 22222 flfval 22526 cnmpt2plusg 22624 cnmpt2vsca 22730 ustincl 22743 xbln0 22951 blssec 22972 blpnfctr 22973 mopni2 23030 mopni3 23031 nmoval 23251 nmocl 23256 isnghm2 23260 isnmhm2 23288 cnmpt2ds 23378 metdseq0 23389 cnmpt2ip 23778 caucfil 23813 mbfimasn 24160 dvnf 24451 dvnbss 24452 coemul 24769 dvply1 24800 dvnply2 24803 pserdvlem2 24943 logeftb 25094 advlogexp 25165 cxpne0 25187 cxpp1 25190 f1otrg 26584 ax5seglem9 26650 uhgrn0 26779 upgrn0 26801 upgrle 26802 uhgrwkspthlem2 27462 frgrhash2wsp 28038 sspval 28427 sspnval 28441 lnof 28459 nmooval 28467 nmooge0 28471 nmoub3i 28477 bloln 28488 nmblore 28490 hosval 29444 homval 29445 hodval 29446 hfsval 29447 hfmval 29448 homulass 29506 hoadddir 29508 nmopub2tALT 29613 nmfnleub2 29630 kbval 29658 lnopmul 29671 0lnfn 29689 lnopcoi 29707 nmcoplb 29734 nmcfnlb 29758 kbass2 29821 nmopleid 29843 hstoh 29936 mdi 29999 dmdi 30006 dmdi4 30011 supxrnemnf 30419 reofld 30840 lbsdiflsp0 30921 bnj605 32078 bnj607 32087 bnj1097 32150 cusgredgex 32265 elno2 33058 topdifinffinlem 34510 lindsdom 34767 lindsenlbs 34768 ftc1anclem2 34849 fzmul 34897 nninfnub 34907 exidreslem 35036 grposnOLD 35041 ghomf 35049 rngohomf 35125 rngohom1 35127 rngohomadd 35128 rngohommul 35129 rngoiso1o 35138 rngoisohom 35139 igenmin 35223 lkrcl 36108 lkrf0 36109 omlfh1N 36274 tendoex 37991 3anrabdioph 39257 3orrabdioph 39258 rencldnfilem 39295 dvdsabsmod0 39462 jm2.18 39463 jm2.25 39474 jm2.15nn0 39478 addrfv 40678 subrfv 40679 mulvfv 40680 bi3impa 40695 ssfiunibd 41452 supminfxr 41616 limsupgtlem 41934 xlimmnfv 41991 xlimpnfv 41995 dvnmul 42104 stoweidlem34 42196 stoweidlem48 42210 sge0cl 42540 sge0xp 42588 ovnsubaddlem1 42729 aovmpt4g 43277 gboge9 43806 |
Copyright terms: Public domain | W3C validator |