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  3255  vtocl3gf  3539  vtocl3g  3541  rspc2ev  3601  reuss  4290  frc  5601  trssord  6349  funtp  6573  resdif  6821  f1cdmsn  7257  f1ofvswap  7281  fnotovb  7439  fovcdm  7559  fnovrn  7564  fmpoco  8074  smoord  8334  odi  8543  oeoa  8561  oeoe  8563  nndi  8587  ecopovtrn  8793  ecovass  8797  ecovdi  8798  unfi  9135  entrfil  9149  domtrfil  9156  f1imaenfi  9159  suppr  9423  infpr  9456  harval2  9950  fin23lem31  10296  tskuni  10736  addasspi  10848  mulasspi  10850  distrpi  10851  mulcanenq  10913  genpass  10962  distrlem1pr  10978  prlem934  10986  ltapr  10998  le2tri3i  11304  subadd  11424  addsub  11432  subdi  11611  submul2  11618  ltaddsub  11652  leaddsub  11654  divval  11839  diveq0  11847  div12  11859  diveq1  11867  divneg  11874  divdiv2  11894  ltmulgt11  12042  gt0div  12049  ge0div  12050  uzind3  12628  fnn0ind  12633  qdivcl  12929  irrmul  12933  xrlttr  13100  fzen  13502  modcyc  13868  modcyc2  13869  rpexpmord  14133  faclbnd4lem4  14261  ccatval21sw  14550  lswccatn0lsw  14556  ccatpfx  14666  ccatopth  14681  cshweqdifid  14785  lenegsq  15287  moddvds  16233  dvdscmulr  16254  dvdsmulcr  16255  dvds2add  16260  dvds2sub  16261  dvdsleabs  16281  divalg  16373  divalgb  16374  ndvdsadd  16380  gcdcllem3  16471  dvdslegcd  16474  modgcd  16502  absmulgcd  16519  odzval  16762  pcmul  16822  ressid2  17204  ressval2  17205  catcisolem  18072  prf1st  18165  prf2nd  18166  1st2ndprf  18167  curfuncf  18199  curf2ndf  18208  pltval  18291  pospo  18304  lubel  18473  isdlat  18481  submgmcl  18634  prdssgrpd  18660  issubmnd  18688  prdsmndd  18697  submcl  18739  grpinvid1  18923  grpinvid2  18924  mulgp1  19039  ghmlin  19153  ghmsub  19156  odlem2  19469  gexlem2  19512  lsmvalx  19569  efgtval  19653  cmncom  19728  lssvnegcl  20862  islss3  20865  prdslmodd  20875  zntoslem  21466  evlslem2  21986  evlseu  21990  maducoeval2  22527  madutpos  22529  madugsum  22530  madurid  22531  m2cpminvid  22640  pm2mpghm  22703  unopn  22790  ntrss  22942  innei  23012  t1sep2  23256  metustsym  24443  cncfi  24787  rrxds  25293  quotval  26200  abelthlem2  26342  mudivsum  27441  padicabv  27541  nosupfv  27618  nosupres  27619  noinffv  27633  ssltsepc  27705  divsval  28092  axsegconlem1  28844  nsnlplig  30410  nsnlpligALT  30411  grpoinvid1  30457  grpoinvid2  30458  grpodivval  30464  ablo4  30479  ablonncan  30485  nvnpcan  30585  nvmeq0  30587  nvabs  30601  imsdval  30615  ipval  30632  nmorepnf  30697  blo3i  30731  blometi  30732  ipasslem5  30764  hvmulcan  31001  his5  31015  his7  31019  his2sub2  31022  hhssabloilem  31190  hhssnv  31193  fh1  31547  fh2  31548  cm2j  31549  homcl  31675  homco1  31730  homulass  31731  hoadddi  31732  hosubsub2  31741  braadd  31874  bramul  31875  lnopmul  31896  lnopli  31897  lnopaddmuli  31902  lnopsubmuli  31904  lnfnli  31969  lnfnaddmuli  31974  kbass2  32046  mdexchi  32264  xdivval  32839  resvid2  33302  resvval2  33303  fedgmullem2  33626  unitdivcld  33891  bnj229  34874  bnj546  34886  bnj570  34895  cusgredgex2  35110  loop1cycl  35124  cvmlift2lem7  35296  finminlem  36306  ivthALT  36323  topdifinffinlem  37335  lindsadd  37607  exidcl  37870  grposnOLD  37876  rngoneglmul  37937  rngonegrmul  37938  divrngcl  37951  crngocom  37995  crngm4  37997  inidl  38024  xrninxpex  38380  oposlem  39175  hlsuprexch  39375  ldilcnv  40109  ltrnu  40115  tgrpgrplem  40743  tgrpabl  40745  erngdvlem3  40984  erngdvlem3-rN  40992  dvalveclem  41019  dvhfvadd  41085  dvhgrp  41101  dvhlveclem  41102  djhval2  41393  f1o2d2  42221  fmpocos  42222  resubadd  42367  diophren  42801  monotoddzzfi  42931  ltrmynn0  42937  ltrmxnn0  42938  lermxnn0  42939  rmyeq  42943  lermy  42944  jm2.21  42983  radcnvrat  44303  dvconstbi  44323  expgrowth  44324  bi3impb  44474  xlimmnfvlem2  45831  xlimpnfvlem2  45835  fnotaovb  47199  tposcurf1  49288  precofvalALT  49357  onetansqsecsq  49750