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 424 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1112 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ 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 210 df-an 400 df-3an 1090 |
This theorem is referenced by: 3adant3 1133 3impdi 1351 rsp2e 3214 vtocl3gf 3474 rspc2ev 3536 reuss 4202 frc 5485 trssord 6183 funtp 6390 resdif 6632 f1ofvswap 7067 fnotovb 7214 fovrn 7328 fnovrn 7333 fmpoco 7809 smoord 8024 odi 8229 oeoa 8247 oeoe 8249 nndi 8273 ecopovtrn 8424 ecovass 8428 ecovdi 8429 unfi 8764 entrfil 8776 suppr 9001 infpr 9033 harval2 9492 fin23lem31 9836 tskuni 10276 addasspi 10388 mulasspi 10390 distrpi 10391 mulcanenq 10453 genpass 10502 distrlem1pr 10518 prlem934 10526 ltapr 10538 le2tri3i 10841 subadd 10960 addsub 10968 subdi 11144 submul2 11151 ltaddsub 11185 leaddsub 11187 divval 11371 div12 11391 diveq1 11402 divneg 11403 divdiv2 11423 ltmulgt11 11571 gt0div 11577 ge0div 11578 uzind3 12150 fnn0ind 12155 qdivcl 12445 irrmul 12449 xrlttr 12609 fzen 13008 modcyc 13358 modcyc2 13359 rpexpmord 13617 faclbnd4lem4 13741 ccatval21sw 14021 lswccatn0lsw 14027 ccatpfx 14145 ccatopth 14160 cshweqdifid 14264 lenegsq 14763 moddvds 15703 dvdscmulr 15723 dvdsmulcr 15724 dvds2add 15728 dvds2sub 15729 dvdsleabs 15749 divalg 15841 divalgb 15842 ndvdsadd 15848 gcdcllem3 15937 dvdslegcd 15940 modgcd 15969 absmulgcd 15986 odzval 16221 pcmul 16281 ressid2 16648 ressval2 16649 catcisolem 17475 prf1st 17563 prf2nd 17564 1st2ndprf 17565 curfuncf 17597 curf2ndf 17606 pltval 17679 pospo 17692 lubel 17841 isdlat 17912 issubmnd 18047 prdsmndd 18053 submcl 18086 grpinvid1 18265 grpinvid2 18266 mulgp1 18371 ghmlin 18474 ghmsub 18477 odlem2 18778 gexlem2 18818 lsmvalx 18875 efgtval 18960 cmncom 19034 lssvnegcl 19840 islss3 19843 prdslmodd 19853 zntoslem 20368 evlslem2 20886 evlseu 20890 maducoeval2 21384 madutpos 21386 madugsum 21387 madurid 21388 m2cpminvid 21497 pm2mpghm 21560 unopn 21647 ntrss 21799 innei 21869 t1sep2 22113 metustsym 23301 cncfi 23639 rrxds 24138 quotval 25032 abelthlem2 25171 mudivsum 26258 padicabv 26358 axsegconlem1 26855 nsnlplig 28408 nsnlpligALT 28409 grpoinvid1 28455 grpoinvid2 28456 grpodivval 28462 ablo4 28477 ablonncan 28483 nvnpcan 28583 nvmeq0 28585 nvabs 28599 imsdval 28613 ipval 28630 nmorepnf 28695 blo3i 28729 blometi 28730 ipasslem5 28762 hvmulcan 28999 his5 29013 his7 29017 his2sub2 29020 hhssabloilem 29188 hhssnv 29191 fh1 29545 fh2 29546 cm2j 29547 homcl 29673 homco1 29728 homulass 29729 hoadddi 29730 hosubsub2 29739 braadd 29872 bramul 29873 lnopmul 29894 lnopli 29895 lnopaddmuli 29900 lnopsubmuli 29902 lnfnli 29967 lnfnaddmuli 29972 kbass2 30044 mdexchi 30262 xdivval 30760 resvid2 31096 resvval2 31097 fedgmullem2 31275 unitdivcld 31415 bnj229 32427 bnj546 32439 bnj570 32448 cusgredgex2 32647 loop1cycl 32662 cvmlift2lem7 32834 nosupfv 33542 nosupres 33543 noinffv 33557 ssltsepc 33620 finminlem 34137 ivthALT 34154 topdifinffinlem 35130 lindsadd 35382 exidcl 35646 grposnOLD 35652 rngoneglmul 35713 rngonegrmul 35714 divrngcl 35727 crngocom 35771 crngm4 35773 inidl 35800 xrninxpex 36132 oposlem 36808 hlsuprexch 37007 ldilcnv 37741 ltrnu 37747 tgrpgrplem 38375 tgrpabl 38377 erngdvlem3 38616 erngdvlem3-rN 38624 dvalveclem 38651 dvhfvadd 38717 dvhgrp 38733 dvhlveclem 38734 djhval2 39025 resubadd 39923 diophren 40191 monotoddzzfi 40320 ltrmynn0 40326 ltrmxnn0 40327 lermxnn0 40328 rmyeq 40332 lermy 40333 jm2.21 40372 radcnvrat 41454 dvconstbi 41474 expgrowth 41475 bi3impb 41625 eel132 41844 xlimmnfvlem2 42900 xlimpnfvlem2 42904 fnotaovb 44207 submgmcl 44866 onetansqsecsq 45900 |
Copyright terms: Public domain | W3C validator |