Theorem 3impb 1116

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 422	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1112	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3adant3  1133  3impdi  1351  rsp2e  3276  vtocl3gf  3562  vtocl3g  3564  rspc2ev  3624  reuss  4316  frc  5642  trssord  6379  funtp  6603  resdif  6852  f1cdmsn  7277  f1ofvswap  7301  fnotovb  7456  fovcdm  7574  fnovrn  7579  fmpoco  8078  smoord  8362  odi  8576  oeoa  8594  oeoe  8596  nndi  8620  ecopovtrn  8811  ecovass  8815  ecovdi  8816  unfi  9169  entrfil  9185  domtrfil  9192  f1imaenfi  9195  suppr  9463  infpr  9495  harval2  9989  fin23lem31  10335  tskuni  10775  addasspi  10887  mulasspi  10889  distrpi  10890  mulcanenq  10952  genpass  11001  distrlem1pr  11017  prlem934  11025  ltapr  11037  le2tri3i  11341  subadd  11460  addsub  11468  subdi  11644  submul2  11651  ltaddsub  11685  leaddsub  11687  divval  11871  div12  11891  diveq1  11902  divneg  11903  divdiv2  11923  ltmulgt11  12071  gt0div  12077  ge0div  12078  uzind3  12653  fnn0ind  12658  qdivcl  12951  irrmul  12955  xrlttr  13116  fzen  13515  modcyc  13868  modcyc2  13869  rpexpmord  14130  faclbnd4lem4  14253  ccatval21sw  14532  lswccatn0lsw  14538  ccatpfx  14648  ccatopth  14663  cshweqdifid  14767  lenegsq  15264  moddvds  16205  dvdscmulr  16225  dvdsmulcr  16226  dvds2add  16230  dvds2sub  16231  dvdsleabs  16251  divalg  16343  divalgb  16344  ndvdsadd  16350  gcdcllem3  16439  dvdslegcd  16442  modgcd  16471  absmulgcd  16488  odzval  16721  pcmul  16781  ressid2  17174  ressval2  17175  catcisolem  18057  prf1st  18153  prf2nd  18154  1st2ndprf  18155  curfuncf  18188  curf2ndf  18197  pltval  18282  pospo  18295  lubel  18464  isdlat  18472  prdssgrpd  18621  issubmnd  18649  prdsmndd  18655  submcl  18690  grpinvid1  18873  grpinvid2  18874  mulgp1  18982  ghmlin  19092  ghmsub  19095  odlem2  19402  gexlem2  19445  lsmvalx  19502  efgtval  19586  cmncom  19661  lssvnegcl  20560  islss3  20563  prdslmodd  20573  zntoslem  21104  evlslem2  21634  evlseu  21638  maducoeval2  22134  madutpos  22136  madugsum  22137  madurid  22138  m2cpminvid  22247  pm2mpghm  22310  unopn  22397  ntrss  22551  innei  22621  t1sep2  22865  metustsym  24056  cncfi  24402  rrxds  24902  quotval  25797  abelthlem2  25936  mudivsum  27023  padicabv  27123  nosupfv  27199  nosupres  27200  noinffv  27214  ssltsepc  27284  divsval  27627  axsegconlem1  28165  nsnlplig  29722  nsnlpligALT  29723  grpoinvid1  29769  grpoinvid2  29770  grpodivval  29776  ablo4  29791  ablonncan  29797  nvnpcan  29897  nvmeq0  29899  nvabs  29913  imsdval  29927  ipval  29944  nmorepnf  30009  blo3i  30043  blometi  30044  ipasslem5  30076  hvmulcan  30313  his5  30327  his7  30331  his2sub2  30334  hhssabloilem  30502  hhssnv  30505  fh1  30859  fh2  30860  cm2j  30861  homcl  30987  homco1  31042  homulass  31043  hoadddi  31044  hosubsub2  31053  braadd  31186  bramul  31187  lnopmul  31208  lnopli  31209  lnopaddmuli  31214  lnopsubmuli  31216  lnfnli  31281  lnfnaddmuli  31286  kbass2  31358  mdexchi  31576  xdivval  32073  resvid2  32431  resvval2  32432  fedgmullem2  32704  unitdivcld  32870  bnj229  33884  bnj546  33896  bnj570  33905  cusgredgex2  34102  loop1cycl  34117  cvmlift2lem7  34289  finminlem  35192  ivthALT  35209  topdifinffinlem  36217  lindsadd  36470  exidcl  36733  grposnOLD  36739  rngoneglmul  36800  rngonegrmul  36801  divrngcl  36814  crngocom  36858  crngm4  36860  inidl  36887  xrninxpex  37253  oposlem  38041  hlsuprexch  38241  ldilcnv  38975  ltrnu  38981  tgrpgrplem  39609  tgrpabl  39611  erngdvlem3  39850  erngdvlem3-rN  39858  dvalveclem  39885  dvhfvadd  39951  dvhgrp  39967  dvhlveclem  39968  djhval2  40259  f1o2d2  41053  fmpocos  41054  resubadd  41249  diophren  41537  monotoddzzfi  41667  ltrmynn0  41673  ltrmxnn0  41674  lermxnn0  41675  rmyeq  41679  lermy  41680  jm2.21  41719  radcnvrat  43059  dvconstbi  43079  expgrowth  43080  bi3impb  43230  eel132  43449  xlimmnfvlem2  44536  xlimpnfvlem2  44540  fnotaovb  45893  submgmcl  46551  onetansqsecsq  47760