Theorem 3impb 1114

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 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant3  1132  syl3an132  1166  3impdi  1351  rsp2e  3253  vtocl3gf  3536  vtocl3g  3538  rspc2ev  3598  reuss  4286  frc  5594  trssord  6337  funtp  6557  resdif  6803  f1cdmsn  7239  f1ofvswap  7263  fnotovb  7421  fovcdm  7539  fnovrn  7544  fmpoco  8051  smoord  8311  odi  8520  oeoa  8538  oeoe  8540  nndi  8564  ecopovtrn  8770  ecovass  8774  ecovdi  8775  unfi  9112  entrfil  9126  domtrfil  9133  f1imaenfi  9136  suppr  9399  infpr  9432  harval2  9926  fin23lem31  10272  tskuni  10712  addasspi  10824  mulasspi  10826  distrpi  10827  mulcanenq  10889  genpass  10938  distrlem1pr  10954  prlem934  10962  ltapr  10974  le2tri3i  11280  subadd  11400  addsub  11408  subdi  11587  submul2  11594  ltaddsub  11628  leaddsub  11630  divval  11815  diveq0  11823  div12  11835  diveq1  11843  divneg  11850  divdiv2  11870  ltmulgt11  12018  gt0div  12025  ge0div  12026  uzind3  12604  fnn0ind  12609  qdivcl  12905  irrmul  12909  xrlttr  13076  fzen  13478  modcyc  13844  modcyc2  13845  rpexpmord  14109  faclbnd4lem4  14237  ccatval21sw  14526  lswccatn0lsw  14532  ccatpfx  14642  ccatopth  14657  cshweqdifid  14761  lenegsq  15263  moddvds  16209  dvdscmulr  16230  dvdsmulcr  16231  dvds2add  16236  dvds2sub  16237  dvdsleabs  16257  divalg  16349  divalgb  16350  ndvdsadd  16356  gcdcllem3  16447  dvdslegcd  16450  modgcd  16478  absmulgcd  16495  odzval  16738  pcmul  16798  ressid2  17180  ressval2  17181  catcisolem  18048  prf1st  18141  prf2nd  18142  1st2ndprf  18143  curfuncf  18175  curf2ndf  18184  pltval  18267  pospo  18280  lubel  18449  isdlat  18457  submgmcl  18610  prdssgrpd  18636  issubmnd  18664  prdsmndd  18673  submcl  18715  grpinvid1  18899  grpinvid2  18900  mulgp1  19015  ghmlin  19129  ghmsub  19132  odlem2  19445  gexlem2  19488  lsmvalx  19545  efgtval  19629  cmncom  19704  lssvnegcl  20838  islss3  20841  prdslmodd  20851  zntoslem  21442  evlslem2  21962  evlseu  21966  maducoeval2  22503  madutpos  22505  madugsum  22506  madurid  22507  m2cpminvid  22616  pm2mpghm  22679  unopn  22766  ntrss  22918  innei  22988  t1sep2  23232  metustsym  24419  cncfi  24763  rrxds  25269  quotval  26176  abelthlem2  26318  mudivsum  27417  padicabv  27517  nosupfv  27594  nosupres  27595  noinffv  27609  ssltsepc  27681  divsval  28068  axsegconlem1  28820  nsnlplig  30383  nsnlpligALT  30384  grpoinvid1  30430  grpoinvid2  30431  grpodivval  30437  ablo4  30452  ablonncan  30458  nvnpcan  30558  nvmeq0  30560  nvabs  30574  imsdval  30588  ipval  30605  nmorepnf  30670  blo3i  30704  blometi  30705  ipasslem5  30737  hvmulcan  30974  his5  30988  his7  30992  his2sub2  30995  hhssabloilem  31163  hhssnv  31166  fh1  31520  fh2  31521  cm2j  31522  homcl  31648  homco1  31703  homulass  31704  hoadddi  31705  hosubsub2  31714  braadd  31847  bramul  31848  lnopmul  31869  lnopli  31870  lnopaddmuli  31875  lnopsubmuli  31877  lnfnli  31942  lnfnaddmuli  31947  kbass2  32019  mdexchi  32237  xdivval  32812  resvid2  33275  resvval2  33276  fedgmullem2  33599  unitdivcld  33864  bnj229  34847  bnj546  34859  bnj570  34868  cusgredgex2  35083  loop1cycl  35097  cvmlift2lem7  35269  finminlem  36279  ivthALT  36296  topdifinffinlem  37308  lindsadd  37580  exidcl  37843  grposnOLD  37849  rngoneglmul  37910  rngonegrmul  37911  divrngcl  37924  crngocom  37968  crngm4  37970  inidl  37997  xrninxpex  38353  oposlem  39148  hlsuprexch  39348  ldilcnv  40082  ltrnu  40088  tgrpgrplem  40716  tgrpabl  40718  erngdvlem3  40957  erngdvlem3-rN  40965  dvalveclem  40992  dvhfvadd  41058  dvhgrp  41074  dvhlveclem  41075  djhval2  41366  f1o2d2  42194  fmpocos  42195  resubadd  42340  diophren  42774  monotoddzzfi  42904  ltrmynn0  42910  ltrmxnn0  42911  lermxnn0  42912  rmyeq  42916  lermy  42917  jm2.21  42956  radcnvrat  44276  dvconstbi  44296  expgrowth  44297  bi3impb  44447  xlimmnfvlem2  45804  xlimpnfvlem2  45808  fnotaovb  47172  tposcurf1  49261  precofvalALT  49330  onetansqsecsq  49723