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  3625  reuss  4317  frc  5643  trssord  6382  funtp  6606  resdif  6855  f1cdmsn  7280  f1ofvswap  7304  fnotovb  7459  fovcdm  7577  fnovrn  7582  fmpoco  8081  smoord  8365  odi  8579  oeoa  8597  oeoe  8599  nndi  8623  ecopovtrn  8814  ecovass  8818  ecovdi  8819  unfi  9172  entrfil  9188  domtrfil  9195  f1imaenfi  9198  suppr  9466  infpr  9498  harval2  9992  fin23lem31  10338  tskuni  10778  addasspi  10890  mulasspi  10892  distrpi  10893  mulcanenq  10955  genpass  11004  distrlem1pr  11020  prlem934  11028  ltapr  11040  le2tri3i  11344  subadd  11463  addsub  11471  subdi  11647  submul2  11654  ltaddsub  11688  leaddsub  11690  divval  11874  div12  11894  diveq1  11905  divneg  11906  divdiv2  11926  ltmulgt11  12074  gt0div  12080  ge0div  12081  uzind3  12656  fnn0ind  12661  qdivcl  12954  irrmul  12958  xrlttr  13119  fzen  13518  modcyc  13871  modcyc2  13872  rpexpmord  14133  faclbnd4lem4  14256  ccatval21sw  14535  lswccatn0lsw  14541  ccatpfx  14651  ccatopth  14666  cshweqdifid  14770  lenegsq  15267  moddvds  16208  dvdscmulr  16228  dvdsmulcr  16229  dvds2add  16233  dvds2sub  16234  dvdsleabs  16254  divalg  16346  divalgb  16347  ndvdsadd  16353  gcdcllem3  16442  dvdslegcd  16445  modgcd  16474  absmulgcd  16491  odzval  16724  pcmul  16784  ressid2  17177  ressval2  17178  catcisolem  18060  prf1st  18156  prf2nd  18157  1st2ndprf  18158  curfuncf  18191  curf2ndf  18200  pltval  18285  pospo  18298  lubel  18467  isdlat  18475  prdssgrpd  18624  issubmnd  18652  prdsmndd  18658  submcl  18693  grpinvid1  18876  grpinvid2  18877  mulgp1  18987  ghmlin  19097  ghmsub  19100  odlem2  19407  gexlem2  19450  lsmvalx  19507  efgtval  19591  cmncom  19666  lssvnegcl  20567  islss3  20570  prdslmodd  20580  zntoslem  21112  evlslem2  21642  evlseu  21646  maducoeval2  22142  madutpos  22144  madugsum  22145  madurid  22146  m2cpminvid  22255  pm2mpghm  22318  unopn  22405  ntrss  22559  innei  22629  t1sep2  22873  metustsym  24064  cncfi  24410  rrxds  24910  quotval  25805  abelthlem2  25944  mudivsum  27033  padicabv  27133  nosupfv  27209  nosupres  27210  noinffv  27224  ssltsepc  27294  divsval  27637  axsegconlem1  28175  nsnlplig  29734  nsnlpligALT  29735  grpoinvid1  29781  grpoinvid2  29782  grpodivval  29788  ablo4  29803  ablonncan  29809  nvnpcan  29909  nvmeq0  29911  nvabs  29925  imsdval  29939  ipval  29956  nmorepnf  30021  blo3i  30055  blometi  30056  ipasslem5  30088  hvmulcan  30325  his5  30339  his7  30343  his2sub2  30346  hhssabloilem  30514  hhssnv  30517  fh1  30871  fh2  30872  cm2j  30873  homcl  30999  homco1  31054  homulass  31055  hoadddi  31056  hosubsub2  31065  braadd  31198  bramul  31199  lnopmul  31220  lnopli  31221  lnopaddmuli  31226  lnopsubmuli  31228  lnfnli  31293  lnfnaddmuli  31298  kbass2  31370  mdexchi  31588  xdivval  32085  resvid2  32442  resvval2  32443  fedgmullem2  32715  unitdivcld  32881  bnj229  33895  bnj546  33907  bnj570  33916  cusgredgex2  34113  loop1cycl  34128  cvmlift2lem7  34300  finminlem  35203  ivthALT  35220  topdifinffinlem  36228  lindsadd  36481  exidcl  36744  grposnOLD  36750  rngoneglmul  36811  rngonegrmul  36812  divrngcl  36825  crngocom  36869  crngm4  36871  inidl  36898  xrninxpex  37264  oposlem  38052  hlsuprexch  38252  ldilcnv  38986  ltrnu  38992  tgrpgrplem  39620  tgrpabl  39622  erngdvlem3  39861  erngdvlem3-rN  39869  dvalveclem  39896  dvhfvadd  39962  dvhgrp  39978  dvhlveclem  39979  djhval2  40270  f1o2d2  41055  fmpocos  41056  resubadd  41252  diophren  41551  monotoddzzfi  41681  ltrmynn0  41687  ltrmxnn0  41688  lermxnn0  41689  rmyeq  41693  lermy  41694  jm2.21  41733  radcnvrat  43073  dvconstbi  43093  expgrowth  43094  bi3impb  43244  eel132  43463  xlimmnfvlem2  44549  xlimpnfvlem2  44553  fnotaovb  45906  submgmcl  46564  onetansqsecsq  47806