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 629 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1249 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: 3adant1l 1310 3adant1r 1311 3impdi 1373 rsp2e 2987 vtocl3gf 3242 rspc2ev 3295 reuss 3867 frc 5004 trssord 5657 funtp 5859 resdif 6070 fnotovb 6592 fovrn 6702 fnovrn 6707 fmpt2co 7147 smoord 7349 odi 7546 oeoa 7564 oeoe 7566 nndi 7590 ecopovtrn 7737 ecovass 7742 ecovdi 7743 suppr 8260 infpr 8292 harval2 8706 cdaassen 8887 fin23lem31 9048 tskuni 9484 addasspi 9596 mulasspi 9598 distrpi 9599 mulcanenq 9661 genpass 9710 distrlem1pr 9726 prlem934 9734 ltapr 9746 le2tri3i 10046 subadd 10163 addsub 10171 subdi 10342 submul2 10349 ltaddsub 10381 leaddsub 10383 divval 10566 div12 10586 diveq1 10597 divneg 10598 divdiv2 10616 ltmulgt11 10762 gt0div 10768 ge0div 10769 uzind3 11347 fnn0ind 11352 qdivcl 11685 irrmul 11689 xrlttr 11849 fzen 12229 modcyc 12567 modcyc2 12568 faclbnd4lem4 12945 cshweqdifid 13417 lenegsq 13908 moddvds 14829 dvdscmulr 14848 dvdsmulcr 14849 dvds2add 14853 dvds2sub 14854 dvdsleabs 14871 divalg 14964 divalgb 14965 ndvdsadd 14972 gcdcllem3 15061 dvdslegcd 15064 modgcd 15091 absmulgcd 15104 odzval 15334 pcmul 15394 ressid2 15755 ressval2 15756 catcisolem 16579 prf1st 16667 prf2nd 16668 1st2ndprf 16669 curfuncf 16701 curf2ndf 16710 pltval 16783 pospo 16796 lubel 16945 isdlat 17016 issubmnd 17141 prdsmndd 17146 submcl 17176 grpinvid1 17293 grpinvid2 17294 mulgp1 17397 ghmlin 17488 ghmsub 17491 odlem2 17781 gexlem2 17820 lsmvalx 17877 efgtval 17959 cmncom 18032 lssvnegcl 18777 islss3 18780 prdslmodd 18790 evlslem2 19333 evlseu 19337 zntoslem 19724 maducoeval2 20265 madutpos 20267 madugsum 20268 madurid 20269 m2cpminvid 20377 pm2mpghm 20440 unopn 20533 ntrss 20669 innei 20739 t1sep2 20983 metustsym 22170 cncfi 22505 rrxds 22989 quotval 23851 abelthlem2 23990 mudivsum 25019 padicabv 25119 axsegconlem1 25597 frgregordn0 26597 grpoinvid1 26766 grpoinvid2 26767 grpodivval 26773 ablo4 26788 ablonncan 26795 nvnpcan 26895 nvmeq0 26897 nvabs 26911 imsdval 26925 ipval 26942 nmorepnf 27007 blo3i 27041 blometi 27042 ipasslem5 27074 hvmulcan 27313 his5 27327 his7 27331 his2sub2 27334 hhssabloilem 27502 hhssnv 27505 fh1 27861 fh2 27862 cm2j 27863 homcl 27989 homco1 28044 homulass 28045 hoadddi 28046 hosubsub2 28055 braadd 28188 bramul 28189 lnopmul 28210 lnopli 28211 lnopaddmuli 28216 lnopsubmuli 28218 lnfnli 28283 lnfnaddmuli 28288 kbass2 28360 mdexchi 28578 xdivval 28958 resvid2 29159 resvval2 29160 unitdivcld 29275 bnj229 30208 bnj546 30220 bnj570 30229 cvmlift2lem7 30545 finminlem 31482 ivthALT 31500 topdifinffinlem 32371 exidcl 32845 grposnOLD 32851 rngoneglmul 32912 rngonegrmul 32913 divrngcl 32926 crngocom 32970 crngm4 32972 inidl 32999 oposlem 33487 hlsuprexch 33685 ldilcnv 34419 ltrnu 34425 tgrpgrplem 35055 tgrpabl 35057 erngdvlem3 35296 erngdvlem3-rN 35304 dvalveclem 35332 dvhfvadd 35398 dvhgrp 35414 dvhlveclem 35415 djhval2 35706 diophren 36395 monotoddzzfi 36525 rpexpmord 36531 ltrmynn0 36533 ltrmxnn0 36534 lermxnn0 36535 rmyeq 36539 lermy 36540 jm2.21 36579 radcnvrat 37535 dvconstbi 37555 expgrowth 37556 bi3impb 37710 eel132 37948 fnotaovb 39927 ccatpfx 40272 frgrhash2wsp 41497 submgmcl 41584 onetansqsecsq 42301 |
Copyright terms: Public domain | W3C validator |