Theorem 3impb 1130

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adant3  1148  syl3an132  1182  3impdi  1367  rsp2e  3289  vtocl3gf  3546  vtocl3g  3548  rspc2ev  3603  reuss  4288  frc  5622  trssord  6374  funtp  6590  resdif  6840  f1cdmsn  7278  f1ofvswap  7302  fnotovb  7460  fovcdm  7578  fnovrn  7583  fmpoco  8086  mpof1o2d  8117  smoord  8348  odi  8560  oeoa  8579  oeoe  8581  nndi  8605  ecopovtrn  8814  ecovass  8818  ecovdi  8819  unfi  9151  entrfil  9165  domtrfil  9172  f1imaenfi  9175  suppr  9428  infpr  9461  harval2  9979  fin23lem31  10323  tskuni  10764  addasspi  10876  mulasspi  10878  distrpi  10879  mulcanenq  10941  genpass  10990  distrlem1pr  11006  prlem934  11014  ltapr  11026  le2tri3i  11336  subadd  11456  addsub  11464  subdi  11643  submul2  11650  ltaddsub  11684  leaddsub  11686  divval  11870  diveq0  11878  div12  11890  diveq1  11897  divneg  11902  divdiv2  11923  ltmulgt11  12070  gt0div  12077  ge0div  12078  uzind3  12686  fnn0ind  12691  qdivcl  12990  irrmul  12994  xrlttr  13161  fzen  13565  modcyc  13935  modcyc2  13936  rpexpmord  14200  faclbnd4lem4  14328  ccatval21sw  14619  lswccatn0lsw  14625  ccatpfx  14734  ccatopth  14749  cshweqdifid  14853  lenegsq  15368  moddvds  16317  dvdscmulr  16338  dvdsmulcr  16339  dvds2add  16344  dvds2sub  16345  dvdsleabs  16365  divalg  16457  divalgb  16458  ndvdsadd  16464  gcdcllem3  16555  dvdslegcd  16558  modgcd  16586  absmulgcd  16603  odzval  16847  pcmul  16907  ressid2  17290  ressval2  17291  catcisolem  18163  prf1st  18256  prf2nd  18257  1st2ndprf  18258  curfuncf  18290  curf2ndf  18299  pltval  18382  pospo  18395  lubel  18566  isdlat  18574  submgmcl  18761  prdssgrpd  18787  issubmnd  18815  prdsmndd  18824  submcl  18866  grpinvid1  19054  grpinvid2  19055  mulgp1  19169  ghmlin  19287  ghmsub  19290  odlem2  19605  gexlem2  19648  lsmvalx  19705  efgtval  19789  cmncom  19864  lssvnegcl  21051  islss3  21054  prdslmodd  21064  zntoslem  21671  evlslem2  22195  evlseu  22199  maducoeval2  22762  madutpos  22764  madugsum  22765  madurid  22766  m2cpminvid  22875  pm2mpghm  22938  unopn  23025  ntrss  23177  innei  23247  t1sep2  23491  metustsym  24677  cncfi  25018  rrxds  25517  quotval  26418  abelthlem2  26557  mudivsum  27656  padicabv  27756  nosupfv  27832  nosupres  27833  noinffv  27847  sltssepc  27926  divsval  28344  axsegconlem1  29204  nsnlplig  30770  nsnlpligALT  30771  grpoinvid1  30817  grpoinvid2  30818  grpodivval  30824  ablo4  30839  ablonncan  30845  nvnpcan  30945  nvmeq0  30947  nvabs  30961  imsdval  30975  ipval  30992  nmorepnf  31057  blo3i  31091  blometi  31092  ipasslem5  31124  hvmulcan  31361  his5  31375  his7  31379  his2sub2  31382  hhssabloilem  31550  hhssnv  31553  fh1  31907  fh2  31908  cm2j  31909  homcl  32035  homco1  32090  homulass  32091  hoadddi  32092  hosubsub2  32101  braadd  32234  bramul  32235  lnopmul  32256  lnopli  32257  lnopaddmuli  32262  lnopsubmuli  32264  lnfnli  32329  lnfnaddmuli  32334  kbass2  32406  mdexchi  32624  xdivval  33175  resvid2  33589  resvval2  33590  fedgmullem2  33961  unitdivcld  34232  bnj229  35213  bnj546  35225  bnj570  35234  rankfilimb  35434  cusgredgex2  35510  loop1cycl  35524  cvmlift2lem7  35696  finminlem  36714  ivthALT  36731  topdifinffinlem  37876  lindsadd  38147  exidcl  38410  grposnOLD  38416  rngoneglmul  38477  rngonegrmul  38478  divrngcl  38491  crngocom  38535  crngm4  38537  inidl  38564  xrninxpex  38951  oposlem  39841  hlsuprexch  40040  ldilcnv  40774  ltrnu  40780  tgrpgrplem  41408  tgrpabl  41410  erngdvlem3  41649  erngdvlem3-rN  41657  dvalveclem  41684  dvhfvadd  41750  dvhgrp  41766  dvhlveclem  41767  djhval2  42058  fmpocos  42887  resubadd  43023  diophren  43425  monotoddzzfi  43554  ltrmynn0  43560  ltrmxnn0  43561  lermxnn0  43562  rmyeq  43566  lermy  43567  jm2.21  43606  radcnvrat  44909  dvconstbi  44929  expgrowth  44930  bi3impb  45078  xlimmnfvlem2  46432  xlimpnfvlem2  46436  fnotaovb  47817  tposcurf1  49955  precofvalALT  50024  onetansqsecsq  50417