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  3256  vtocl3gf  3542  vtocl3g  3544  rspc2ev  3604  reuss  4293  frc  5604  trssord  6352  funtp  6576  resdif  6824  f1cdmsn  7260  f1ofvswap  7284  fnotovb  7442  fovcdm  7562  fnovrn  7567  fmpoco  8077  smoord  8337  odi  8546  oeoa  8564  oeoe  8566  nndi  8590  ecopovtrn  8796  ecovass  8800  ecovdi  8801  unfi  9141  entrfil  9155  domtrfil  9162  f1imaenfi  9165  suppr  9430  infpr  9463  harval2  9957  fin23lem31  10303  tskuni  10743  addasspi  10855  mulasspi  10857  distrpi  10858  mulcanenq  10920  genpass  10969  distrlem1pr  10985  prlem934  10993  ltapr  11005  le2tri3i  11311  subadd  11431  addsub  11439  subdi  11618  submul2  11625  ltaddsub  11659  leaddsub  11661  divval  11846  diveq0  11854  div12  11866  diveq1  11874  divneg  11881  divdiv2  11901  ltmulgt11  12049  gt0div  12056  ge0div  12057  uzind3  12635  fnn0ind  12640  qdivcl  12936  irrmul  12940  xrlttr  13107  fzen  13509  modcyc  13875  modcyc2  13876  rpexpmord  14140  faclbnd4lem4  14268  ccatval21sw  14557  lswccatn0lsw  14563  ccatpfx  14673  ccatopth  14688  cshweqdifid  14792  lenegsq  15294  moddvds  16240  dvdscmulr  16261  dvdsmulcr  16262  dvds2add  16267  dvds2sub  16268  dvdsleabs  16288  divalg  16380  divalgb  16381  ndvdsadd  16387  gcdcllem3  16478  dvdslegcd  16481  modgcd  16509  absmulgcd  16526  odzval  16769  pcmul  16829  ressid2  17211  ressval2  17212  catcisolem  18079  prf1st  18172  prf2nd  18173  1st2ndprf  18174  curfuncf  18206  curf2ndf  18215  pltval  18298  pospo  18311  lubel  18480  isdlat  18488  submgmcl  18641  prdssgrpd  18667  issubmnd  18695  prdsmndd  18704  submcl  18746  grpinvid1  18930  grpinvid2  18931  mulgp1  19046  ghmlin  19160  ghmsub  19163  odlem2  19476  gexlem2  19519  lsmvalx  19576  efgtval  19660  cmncom  19735  lssvnegcl  20869  islss3  20872  prdslmodd  20882  zntoslem  21473  evlslem2  21993  evlseu  21997  maducoeval2  22534  madutpos  22536  madugsum  22537  madurid  22538  m2cpminvid  22647  pm2mpghm  22710  unopn  22797  ntrss  22949  innei  23019  t1sep2  23263  metustsym  24450  cncfi  24794  rrxds  25300  quotval  26207  abelthlem2  26349  mudivsum  27448  padicabv  27548  nosupfv  27625  nosupres  27626  noinffv  27640  ssltsepc  27712  divsval  28099  axsegconlem1  28851  nsnlplig  30417  nsnlpligALT  30418  grpoinvid1  30464  grpoinvid2  30465  grpodivval  30471  ablo4  30486  ablonncan  30492  nvnpcan  30592  nvmeq0  30594  nvabs  30608  imsdval  30622  ipval  30639  nmorepnf  30704  blo3i  30738  blometi  30739  ipasslem5  30771  hvmulcan  31008  his5  31022  his7  31026  his2sub2  31029  hhssabloilem  31197  hhssnv  31200  fh1  31554  fh2  31555  cm2j  31556  homcl  31682  homco1  31737  homulass  31738  hoadddi  31739  hosubsub2  31748  braadd  31881  bramul  31882  lnopmul  31903  lnopli  31904  lnopaddmuli  31909  lnopsubmuli  31911  lnfnli  31976  lnfnaddmuli  31981  kbass2  32053  mdexchi  32271  xdivval  32846  resvid2  33309  resvval2  33310  fedgmullem2  33633  unitdivcld  33898  bnj229  34881  bnj546  34893  bnj570  34902  cusgredgex2  35117  loop1cycl  35131  cvmlift2lem7  35303  finminlem  36313  ivthALT  36330  topdifinffinlem  37342  lindsadd  37614  exidcl  37877  grposnOLD  37883  rngoneglmul  37944  rngonegrmul  37945  divrngcl  37958  crngocom  38002  crngm4  38004  inidl  38031  xrninxpex  38387  oposlem  39182  hlsuprexch  39382  ldilcnv  40116  ltrnu  40122  tgrpgrplem  40750  tgrpabl  40752  erngdvlem3  40991  erngdvlem3-rN  40999  dvalveclem  41026  dvhfvadd  41092  dvhgrp  41108  dvhlveclem  41109  djhval2  41400  f1o2d2  42228  fmpocos  42229  resubadd  42374  diophren  42808  monotoddzzfi  42938  ltrmynn0  42944  ltrmxnn0  42945  lermxnn0  42946  rmyeq  42950  lermy  42951  jm2.21  42990  radcnvrat  44310  dvconstbi  44330  expgrowth  44331  bi3impb  44481  xlimmnfvlem2  45838  xlimpnfvlem2  45842  fnotaovb  47203  tposcurf1  49292  precofvalALT  49361  onetansqsecsq  49754