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  3254  vtocl3gf  3528  vtocl3g  3530  rspc2ev  3589  reuss  4279  frc  5587  trssord  6334  funtp  6549  resdif  6795  f1cdmsn  7228  f1ofvswap  7252  fnotovb  7410  fovcdm  7528  fnovrn  7533  fmpoco  8037  smoord  8297  odi  8506  oeoa  8525  oeoe  8527  nndi  8551  ecopovtrn  8757  ecovass  8761  ecovdi  8762  unfi  9095  entrfil  9109  domtrfil  9116  f1imaenfi  9119  suppr  9375  infpr  9408  harval2  9909  fin23lem31  10253  tskuni  10694  addasspi  10806  mulasspi  10808  distrpi  10809  mulcanenq  10871  genpass  10920  distrlem1pr  10936  prlem934  10944  ltapr  10956  le2tri3i  11263  subadd  11383  addsub  11391  subdi  11570  submul2  11577  ltaddsub  11611  leaddsub  11613  divval  11798  diveq0  11806  div12  11818  diveq1  11826  divneg  11833  divdiv2  11853  ltmulgt11  12001  gt0div  12008  ge0div  12009  uzind3  12586  fnn0ind  12591  qdivcl  12883  irrmul  12887  xrlttr  13054  fzen  13457  modcyc  13826  modcyc2  13827  rpexpmord  14091  faclbnd4lem4  14219  ccatval21sw  14509  lswccatn0lsw  14515  ccatpfx  14624  ccatopth  14639  cshweqdifid  14743  lenegsq  15244  moddvds  16190  dvdscmulr  16211  dvdsmulcr  16212  dvds2add  16217  dvds2sub  16218  dvdsleabs  16238  divalg  16330  divalgb  16331  ndvdsadd  16337  gcdcllem3  16428  dvdslegcd  16431  modgcd  16459  absmulgcd  16476  odzval  16719  pcmul  16779  ressid2  17161  ressval2  17162  catcisolem  18034  prf1st  18127  prf2nd  18128  1st2ndprf  18129  curfuncf  18161  curf2ndf  18170  pltval  18253  pospo  18266  lubel  18437  isdlat  18445  submgmcl  18632  prdssgrpd  18658  issubmnd  18686  prdsmndd  18695  submcl  18737  grpinvid1  18921  grpinvid2  18922  mulgp1  19037  ghmlin  19150  ghmsub  19153  odlem2  19468  gexlem2  19511  lsmvalx  19568  efgtval  19652  cmncom  19727  lssvnegcl  20907  islss3  20910  prdslmodd  20920  zntoslem  21511  evlslem2  22034  evlseu  22038  maducoeval2  22584  madutpos  22586  madugsum  22587  madurid  22588  m2cpminvid  22697  pm2mpghm  22760  unopn  22847  ntrss  22999  innei  23069  t1sep2  23313  metustsym  24499  cncfi  24843  rrxds  25349  quotval  26256  abelthlem2  26398  mudivsum  27497  padicabv  27597  nosupfv  27674  nosupres  27675  noinffv  27689  sltssepc  27767  divsval  28185  axsegconlem1  28990  nsnlplig  30556  nsnlpligALT  30557  grpoinvid1  30603  grpoinvid2  30604  grpodivval  30610  ablo4  30625  ablonncan  30631  nvnpcan  30731  nvmeq0  30733  nvabs  30747  imsdval  30761  ipval  30778  nmorepnf  30843  blo3i  30877  blometi  30878  ipasslem5  30910  hvmulcan  31147  his5  31161  his7  31165  his2sub2  31168  hhssabloilem  31336  hhssnv  31339  fh1  31693  fh2  31694  cm2j  31695  homcl  31821  homco1  31876  homulass  31877  hoadddi  31878  hosubsub2  31887  braadd  32020  bramul  32021  lnopmul  32042  lnopli  32043  lnopaddmuli  32048  lnopsubmuli  32050  lnfnli  32115  lnfnaddmuli  32120  kbass2  32192  mdexchi  32410  xdivval  33000  resvid2  33411  resvval2  33412  fedgmullem2  33787  unitdivcld  34058  bnj229  35040  bnj546  35052  bnj570  35061  rankfilimb  35258  cusgredgex2  35317  loop1cycl  35331  cvmlift2lem7  35503  finminlem  36512  ivthALT  36529  topdifinffinlem  37552  lindsadd  37814  exidcl  38077  grposnOLD  38083  rngoneglmul  38144  rngonegrmul  38145  divrngcl  38158  crngocom  38202  crngm4  38204  inidl  38231  xrninxpex  38602  oposlem  39442  hlsuprexch  39641  ldilcnv  40375  ltrnu  40381  tgrpgrplem  41009  tgrpabl  41011  erngdvlem3  41250  erngdvlem3-rN  41258  dvalveclem  41285  dvhfvadd  41351  dvhgrp  41367  dvhlveclem  41368  djhval2  41659  f1o2d2  42489  fmpocos  42490  resubadd  42634  diophren  43055  monotoddzzfi  43184  ltrmynn0  43190  ltrmxnn0  43191  lermxnn0  43192  rmyeq  43196  lermy  43197  jm2.21  43236  radcnvrat  44555  dvconstbi  44575  expgrowth  44576  bi3impb  44725  xlimmnfvlem2  46077  xlimpnfvlem2  46081  fnotaovb  47444  tposcurf1  49544  precofvalALT  49613  onetansqsecsq  50006