Theorem 3impb 1115

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 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adant3  1133  syl3an132  1167  3impdi  1352  rsp2e  3256  vtocl3gf  3517  vtocl3g  3519  rspc2ev  3578  reuss  4268  frc  5587  trssord  6334  funtp  6549  resdif  6795  f1cdmsn  7230  f1ofvswap  7254  fnotovb  7412  fovcdm  7530  fnovrn  7535  fmpoco  8038  smoord  8298  odi  8507  oeoa  8526  oeoe  8528  nndi  8552  ecopovtrn  8760  ecovass  8764  ecovdi  8765  unfi  9098  entrfil  9112  domtrfil  9119  f1imaenfi  9122  suppr  9378  infpr  9411  harval2  9912  fin23lem31  10256  tskuni  10697  addasspi  10809  mulasspi  10811  distrpi  10812  mulcanenq  10874  genpass  10923  distrlem1pr  10939  prlem934  10947  ltapr  10959  le2tri3i  11267  subadd  11387  addsub  11395  subdi  11574  submul2  11581  ltaddsub  11615  leaddsub  11617  divval  11802  diveq0  11810  div12  11822  diveq1  11830  divneg  11837  divdiv2  11858  ltmulgt11  12006  gt0div  12013  ge0div  12014  uzind3  12614  fnn0ind  12619  qdivcl  12911  irrmul  12915  xrlttr  13082  fzen  13486  modcyc  13856  modcyc2  13857  rpexpmord  14121  faclbnd4lem4  14249  ccatval21sw  14539  lswccatn0lsw  14545  ccatpfx  14654  ccatopth  14669  cshweqdifid  14773  lenegsq  15274  moddvds  16223  dvdscmulr  16244  dvdsmulcr  16245  dvds2add  16250  dvds2sub  16251  dvdsleabs  16271  divalg  16363  divalgb  16364  ndvdsadd  16370  gcdcllem3  16461  dvdslegcd  16464  modgcd  16492  absmulgcd  16509  odzval  16753  pcmul  16813  ressid2  17195  ressval2  17196  catcisolem  18068  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18195  curf2ndf  18204  pltval  18287  pospo  18300  lubel  18471  isdlat  18479  submgmcl  18666  prdssgrpd  18692  issubmnd  18720  prdsmndd  18729  submcl  18771  grpinvid1  18958  grpinvid2  18959  mulgp1  19074  ghmlin  19187  ghmsub  19190  odlem2  19505  gexlem2  19548  lsmvalx  19605  efgtval  19689  cmncom  19764  lssvnegcl  20942  islss3  20945  prdslmodd  20955  zntoslem  21546  evlslem2  22067  evlseu  22071  maducoeval2  22615  madutpos  22617  madugsum  22618  madurid  22619  m2cpminvid  22728  pm2mpghm  22791  unopn  22878  ntrss  23030  innei  23100  t1sep2  23344  metustsym  24530  cncfi  24871  rrxds  25370  quotval  26269  abelthlem2  26410  mudivsum  27507  padicabv  27607  nosupfv  27684  nosupres  27685  noinffv  27699  sltssepc  27777  divsval  28195  axsegconlem1  29000  nsnlplig  30567  nsnlpligALT  30568  grpoinvid1  30614  grpoinvid2  30615  grpodivval  30621  ablo4  30636  ablonncan  30642  nvnpcan  30742  nvmeq0  30744  nvabs  30758  imsdval  30772  ipval  30789  nmorepnf  30854  blo3i  30888  blometi  30889  ipasslem5  30921  hvmulcan  31158  his5  31172  his7  31176  his2sub2  31179  hhssabloilem  31347  hhssnv  31350  fh1  31704  fh2  31705  cm2j  31706  homcl  31832  homco1  31887  homulass  31888  hoadddi  31889  hosubsub2  31898  braadd  32031  bramul  32032  lnopmul  32053  lnopli  32054  lnopaddmuli  32059  lnopsubmuli  32061  lnfnli  32126  lnfnaddmuli  32131  kbass2  32203  mdexchi  32421  xdivval  32993  resvid2  33405  resvval2  33406  fedgmullem2  33790  unitdivcld  34061  bnj229  35042  bnj546  35054  bnj570  35063  rankfilimb  35261  cusgredgex2  35321  loop1cycl  35335  cvmlift2lem7  35507  finminlem  36516  ivthALT  36533  topdifinffinlem  37677  lindsadd  37948  exidcl  38211  grposnOLD  38217  rngoneglmul  38278  rngonegrmul  38279  divrngcl  38292  crngocom  38336  crngm4  38338  inidl  38365  xrninxpex  38752  oposlem  39642  hlsuprexch  39841  ldilcnv  40575  ltrnu  40581  tgrpgrplem  41209  tgrpabl  41211  erngdvlem3  41450  erngdvlem3-rN  41458  dvalveclem  41485  dvhfvadd  41551  dvhgrp  41567  dvhlveclem  41568  djhval2  41859  f1o2d2  42688  fmpocos  42689  resubadd  42825  diophren  43259  monotoddzzfi  43388  ltrmynn0  43394  ltrmxnn0  43395  lermxnn0  43396  rmyeq  43400  lermy  43401  jm2.21  43440  radcnvrat  44759  dvconstbi  44779  expgrowth  44780  bi3impb  44929  xlimmnfvlem2  46279  xlimpnfvlem2  46283  fnotaovb  47658  tposcurf1  49786  precofvalALT  49855  onetansqsecsq  50248