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 1113 by Wolf Lammen, 20-Jun-2022.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3impa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1091 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3impa.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 220 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-3an 1091 |
This theorem is referenced by: 3imp 1113 3adant1 1132 3adant2 1133 ex3 1348 3impdir 1353 syl3an9b 1436 biimp3a 1471 stoic3 1784 rspec3 3130 rspc3v 3547 raltpg 4611 rextpg 4612 disjiun 5037 otthg 5366 3optocl 5641 fun2ssres 6422 funtpg 6432 funssfv 6735 f1elima 7072 ot1stg 7772 ot2ndg 7773 smogt 8101 omord2 8292 omword 8295 oeword 8315 omabslem 8372 ecovass 8503 fpmg 8546 findcard 8838 endjudisj 9779 cfsmolem 9881 ingru 10426 addasspi 10506 mulasspi 10508 ltapi 10514 ltmpi 10515 axpre-ltadd 10778 leltne 10919 dedekind 10992 recextlem2 11460 divdiv32 11537 divdiv1 11540 lble 11781 fnn0ind 12273 supminf 12528 xrleltne 12732 xrmaxeq 12766 xrmineq 12767 iccgelb 12988 elicc4 12999 iccsplit 13070 elfz 13098 modabs 13474 expgt0 13665 expge0 13668 expge1 13669 mulexpz 13672 expp1z 13681 expm1 13682 expmordi 13734 digit1 13801 faclbnd4 13860 faclbnd5 13861 ccatsymb 14136 s3eqs2s1eq 14500 abssubne0 14877 binom 15391 dvds0lem 15825 dvdsnegb 15832 muldvds1 15839 muldvds2 15840 dvdscmulr 15843 dvdsmulcr 15844 divalgmodcl 15965 gcd2n0cl 16065 gcdaddm 16081 lcmdvds 16162 prmdvdsexp 16269 rpexp1i 16277 monpropd 17239 prfval 17703 xpcpropd 17713 curf2ndf 17752 eqglact 18592 mndodcongi 18932 oddvdsnn0 18933 efgi0 19107 efgi1 19108 efgsval2 19120 lss0cl 19980 mpofrlmd 20736 scmatscmid 21400 pmatcollpw3fi1lem1 21680 cnpval 22130 cnf2 22143 cnnei 22176 lfinun 22419 ptpjcn 22505 cnmptk2 22580 flfval 22884 cnmpt2plusg 22982 cnmpt2vsca 23089 ustincl 23102 xbln0 23309 blssec 23330 blpnfctr 23331 mopni2 23388 mopni3 23389 nmoval 23610 nmocl 23615 isnghm2 23619 isnmhm2 23647 cnmpt2ds 23737 metdseq0 23748 cnmpt2ip 24142 caucfil 24177 mbfimasn 24526 dvnf 24821 dvnbss 24822 coemul 25143 dvply1 25174 dvnply2 25177 pserdvlem2 25317 logeftb 25469 advlogexp 25540 cxpne0 25562 cxpp1 25565 f1otrg 26959 ax5seglem9 27025 uhgrn0 27155 upgrn0 27177 upgrle 27178 uhgrwkspthlem2 27838 frgrhash2wsp 28412 sspval 28801 sspnval 28815 lnof 28833 nmooval 28841 nmooge0 28845 nmoub3i 28851 bloln 28862 nmblore 28864 hosval 29818 homval 29819 hodval 29820 hfsval 29821 hfmval 29822 homulass 29880 hoadddir 29882 nmopub2tALT 29987 nmfnleub2 30004 kbval 30032 lnopmul 30045 0lnfn 30063 lnopcoi 30081 nmcoplb 30108 nmcfnlb 30132 kbass2 30195 nmopleid 30217 hstoh 30310 mdi 30373 dmdi 30380 dmdi4 30385 fdifsuppconst 30740 supxrnemnf 30808 reofld 31255 nsgmgclem 31307 rhmimaidl 31320 lbsdiflsp0 31418 zarclsun 31531 zarclsint 31533 bnj605 32597 bnj607 32606 bnj1097 32671 fnrelpredd 32771 cusgredgex 32793 elno2 33591 topdifinffinlem 35252 lindsdom 35506 lindsenlbs 35507 ftc1anclem2 35586 fzmul 35634 nninfnub 35644 exidreslem 35770 grposnOLD 35775 ghomf 35783 rngohomf 35859 rngohom1 35861 rngohomadd 35862 rngohommul 35863 rngoiso1o 35872 rngoisohom 35873 igenmin 35957 lkrcl 36841 lkrf0 36842 omlfh1N 37007 tendoex 38724 uzindd 39717 sticksstones3 39824 sticksstones10 39831 sticksstones12a 39833 sticksstones12 39834 sticksstones17 39839 3anrabdioph 40305 3orrabdioph 40306 rencldnfilem 40343 dvdsabsmod0 40510 jm2.18 40511 jm2.25 40522 jm2.15nn0 40526 addrfv 41758 subrfv 41759 mulvfv 41760 bi3impa 41775 ssfiunibd 42519 supminfxr 42677 limsupgtlem 42991 xlimmnfv 43048 xlimpnfv 43052 dvnmul 43157 stoweidlem34 43248 stoweidlem48 43262 sge0cl 43592 sge0xp 43640 ovnsubaddlem1 43781 aovmpt4g 44363 gboge9 44887 |
Copyright terms: Public domain | W3C validator |