| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3impb | Structured version Visualization version GIF version | ||
| Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
| Ref | Expression |
|---|---|
| 3impb.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| Ref | Expression |
|---|---|
| 3impb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3impb.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 2 | 1 | exp32 420 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| 3 | 2 | 3imp 1111 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3adant3 1133 3impdi 1351 rsp2e 3278 vtocl3gf 3573 vtocl3g 3575 rspc2ev 3635 reuss 4327 frc 5648 trssord 6401 funtp 6623 resdif 6869 f1cdmsn 7302 f1ofvswap 7326 fnotovb 7483 fovcdm 7603 fnovrn 7608 fmpoco 8120 smoord 8405 odi 8617 oeoa 8635 oeoe 8637 nndi 8661 ecopovtrn 8860 ecovass 8864 ecovdi 8865 unfi 9211 entrfil 9225 domtrfil 9232 f1imaenfi 9235 suppr 9511 infpr 9543 harval2 10037 fin23lem31 10383 tskuni 10823 addasspi 10935 mulasspi 10937 distrpi 10938 mulcanenq 11000 genpass 11049 distrlem1pr 11065 prlem934 11073 ltapr 11085 le2tri3i 11391 subadd 11511 addsub 11519 subdi 11696 submul2 11703 ltaddsub 11737 leaddsub 11739 divval 11924 diveq0 11932 div12 11944 diveq1 11952 divneg 11959 divdiv2 11979 ltmulgt11 12127 gt0div 12134 ge0div 12135 uzind3 12712 fnn0ind 12717 qdivcl 13012 irrmul 13016 xrlttr 13182 fzen 13581 modcyc 13946 modcyc2 13947 rpexpmord 14208 faclbnd4lem4 14335 ccatval21sw 14623 lswccatn0lsw 14629 ccatpfx 14739 ccatopth 14754 cshweqdifid 14858 lenegsq 15359 moddvds 16301 dvdscmulr 16322 dvdsmulcr 16323 dvds2add 16327 dvds2sub 16328 dvdsleabs 16348 divalg 16440 divalgb 16441 ndvdsadd 16447 gcdcllem3 16538 dvdslegcd 16541 modgcd 16569 absmulgcd 16586 odzval 16829 pcmul 16889 ressid2 17278 ressval2 17279 catcisolem 18155 prf1st 18249 prf2nd 18250 1st2ndprf 18251 curfuncf 18283 curf2ndf 18292 pltval 18377 pospo 18390 lubel 18559 isdlat 18567 submgmcl 18720 prdssgrpd 18746 issubmnd 18774 prdsmndd 18783 submcl 18825 grpinvid1 19009 grpinvid2 19010 mulgp1 19125 ghmlin 19239 ghmsub 19242 odlem2 19557 gexlem2 19600 lsmvalx 19657 efgtval 19741 cmncom 19816 lssvnegcl 20954 islss3 20957 prdslmodd 20967 zntoslem 21575 evlslem2 22103 evlseu 22107 maducoeval2 22646 madutpos 22648 madugsum 22649 madurid 22650 m2cpminvid 22759 pm2mpghm 22822 unopn 22909 ntrss 23063 innei 23133 t1sep2 23377 metustsym 24568 cncfi 24920 rrxds 25427 quotval 26334 abelthlem2 26476 mudivsum 27574 padicabv 27674 nosupfv 27751 nosupres 27752 noinffv 27766 ssltsepc 27838 divsval 28215 axsegconlem1 28932 nsnlplig 30500 nsnlpligALT 30501 grpoinvid1 30547 grpoinvid2 30548 grpodivval 30554 ablo4 30569 ablonncan 30575 nvnpcan 30675 nvmeq0 30677 nvabs 30691 imsdval 30705 ipval 30722 nmorepnf 30787 blo3i 30821 blometi 30822 ipasslem5 30854 hvmulcan 31091 his5 31105 his7 31109 his2sub2 31112 hhssabloilem 31280 hhssnv 31283 fh1 31637 fh2 31638 cm2j 31639 homcl 31765 homco1 31820 homulass 31821 hoadddi 31822 hosubsub2 31831 braadd 31964 bramul 31965 lnopmul 31986 lnopli 31987 lnopaddmuli 31992 lnopsubmuli 31994 lnfnli 32059 lnfnaddmuli 32064 kbass2 32136 mdexchi 32354 xdivval 32901 resvid2 33354 resvval2 33355 fedgmullem2 33681 unitdivcld 33900 bnj229 34898 bnj546 34910 bnj570 34919 cusgredgex2 35128 loop1cycl 35142 cvmlift2lem7 35314 finminlem 36319 ivthALT 36336 topdifinffinlem 37348 lindsadd 37620 exidcl 37883 grposnOLD 37889 rngoneglmul 37950 rngonegrmul 37951 divrngcl 37964 crngocom 38008 crngm4 38010 inidl 38037 xrninxpex 38395 oposlem 39183 hlsuprexch 39383 ldilcnv 40117 ltrnu 40123 tgrpgrplem 40751 tgrpabl 40753 erngdvlem3 40992 erngdvlem3-rN 41000 dvalveclem 41027 dvhfvadd 41093 dvhgrp 41109 dvhlveclem 41110 djhval2 41401 f1o2d2 42274 fmpocos 42275 resubadd 42409 diophren 42824 monotoddzzfi 42954 ltrmynn0 42960 ltrmxnn0 42961 lermxnn0 42962 rmyeq 42966 lermy 42967 jm2.21 43006 radcnvrat 44333 dvconstbi 44353 expgrowth 44354 bi3impb 44504 eel132 44722 xlimmnfvlem2 45848 xlimpnfvlem2 45852 fnotaovb 47210 tposcurf1 48999 precofvalALT 49063 onetansqsecsq 49280 |
| Copyright terms: Public domain | W3C validator |