Theorem 3impb 1115

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impb.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3impb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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