Theorem 3impb 1132

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3  1150  syl3an132  1184  3impdi  1369  rsp2e  3280  vtocl3gf  3532  vtocl3g  3534  reuss  4272  cotsexgw  5462  frc  5613  trssord  6379  funtp  6598  resdif  6847  f1cdmsn  7291  f1ofvswap  7315  fnotovb  7473  fovcdm  7592  fnovrn  7597  fmpoco  8108  mpof1o2d  8140  smoord  8377  odi  8591  oeoa  8610  oeoe  8612  nndi  8636  ecopovtrn  8845  ecovass  8849  ecovdi  8850  unfi  9190  entrfil  9204  domtrfil  9211  f1imaenfi  9214  suppr  9468  infpr  9501  harval2  10082  fin23lem31  10425  tskuni  10872  addasspi  10984  mulasspi  10986  distrpi  10987  mulcanenq  11049  genpass  11098  distrlem1pr  11114  prlem934  11122  ltapr  11134  le2tri3i  11444  subadd  11564  addsub  11572  subdi  11753  submul2  11760  ltaddsub  11794  leaddsub  11796  divval  11980  diveq0  11988  div12  12000  diveq1  12007  divneg  12012  divdiv2  12033  ltmulgt11  12180  gt0div  12187  ge0div  12188  uzind3  12797  fnn0ind  12802  qdivcl  13102  irrmul  13106  xrlttr  13273  fzen  13678  modcyc  14050  modcyc2  14051  rpexpmord  14315  faclbnd4lem4  14444  ccatval21sw  14735  lswccatn0lsw  14742  ccatpfx  14855  ccatopth  14870  cshweqdifid  14976  lenegsq  15494  moddvds  16439  dvdscmulr  16460  dvdsmulcr  16461  dvds2add  16466  dvds2sub  16467  dvdsleabs  16487  divalg  16579  divalgb  16580  ndvdsadd  16586  gcdcllem3  16677  dvdslegcd  16680  modgcd  16711  absmulgcd  16728  odzval  16975  pcmul  17035  ressid2  17418  ressval2  17419  catcisolem  18291  prf1st  18384  prf2nd  18385  1st2ndprf  18386  curfuncf  18418  curf2ndf  18427  pltval  18510  pospo  18523  lubel  18694  isdlat  18702  submgmcl  18902  prdssgrpd  18928  issubmnd  18959  prdsmndd  18970  submcl  19013  grpinvid1  19208  grpinvid2  19209  mulgp1  19323  ghmlin  19441  ghmsub  19444  odlem2  19759  gexlem2  19802  lsmvalx  19859  efgtval  19943  cmncom  20018  lssvnegcl  21237  islss3  21240  prdslmodd  21250  zntoslem  21868  evlslem2  22394  evlseu  22398  maducoeval2  22961  madutpos  22963  madugsum  22964  madurid  22965  m2cpminvid  23077  pm2mpghm  23140  unopn  23227  ntrss  23379  innei  23449  t1sep2  23693  metustsym  24880  cncfi  25221  rrxds  25720  quotval  26619  abelthlem2  26765  mudivsum  27863  padicabv  27963  nosupfv  28069  nosupres  28070  noinffv  28084  sltssepc  28163  divsval  28581  axsegconlem1  29501  loop1cycl  30750  nsnlplig  31089  nsnlpligALT  31090  grpoinvid1  31136  grpoinvid2  31137  grpodivval  31143  ablo4  31158  ablonncan  31164  nvnpcan  31264  nvmeq0  31266  nvabs  31280  imsdval  31294  ipval  31311  nmorepnf  31376  blo3i  31410  blometi  31411  ipasslem5  31443  hvmulcan  31680  his5  31694  his7  31698  his2sub2  31701  hhssabloilem  31869  hhssnv  31872  fh1  32226  fh2  32227  cm2j  32228  homcl  32354  homco1  32409  homulass  32410  hoadddi  32411  hosubsub2  32420  braadd  32553  bramul  32554  lnopmul  32575  lnopli  32576  lnopaddmuli  32581  lnopsubmuli  32583  lnfnli  32648  lnfnaddmuli  32653  kbass2  32725  mdexchi  32943  xdivval  33532  resvid2  33938  resvval2  33939  fedgmullem2  34309  unitdivcld  34580  bnj229  35561  bnj546  35573  bnj570  35582  rankfilimb  35781  cusgredgex2  35984  cvmlift2lem7  36161  finminlem  37199  ivthALT  37216  topdifinffinlem  38364  lindsadd  38630  exidcl  38904  grposnOLD  38910  rngoneglmul  38971  rngonegrmul  38972  divrngcl  38985  crngocom  39029  crngm4  39031  inidl  39058  xrninxpex  39443  oposlem  40333  hlsuprexch  40532  ldilcnv  41266  ltrnu  41272  tgrpgrplem  41900  tgrpabl  41902  erngdvlem3  42141  erngdvlem3-rN  42149  dvalveclem  42176  dvhfvadd  42242  dvhgrp  42258  dvhlveclem  42259  djhval2  42550  fmpocos  43381  resubadd  43524  diophren  43914  monotoddzzfi  44043  ltrmynn0  44049  ltrmxnn0  44050  lermxnn0  44051  rmyeq  44055  lermy  44056  jm2.21  44095  radcnvrat  45392  dvconstbi  45412  expgrowth  45413  bi3impb  45561  xlimmnfvlem2  46937  xlimpnfvlem2  46941  fnotaovb  48362  tposcurf1  50515  precofvalALT  50597  onetansqsecsq  51023