Theorem 3expb 1118

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expb	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1117	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 418	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3expia  1119  3adant3r1  1180  3adant3r2  1181  3adant3r3  1182  mp3an1  1446  sotri  6021  fnfco  6623  mpoeq3dva  7330  oprres  7418  fovrnda  7421  fnmpoovd  7898  offval22  7899  bropfvvvvlem  7902  fnsuppres  7978  suppsssn  7988  sprmpod  8011  oaass  8354  omlimcl  8371  odi  8372  nnmsucr  8418  unfi  8917  cflim2  9950  mulcanenq  10647  mul4  11073  add4  11125  2addsub  11165  addsubeq4  11166  subadd4  11195  muladd  11337  ltleadd  11388  divmul  11566  divne0  11575  div23  11582  div12  11585  divsubdir  11599  subdivcomb1  11600  divcan5  11607  divmuleq  11610  divcan6  11612  divdiv32  11613  div2sub  11730  letrp1  11749  lemul12b  11762  lediv1  11770  lt2mul2div  11783  lemuldiv  11785  ltdiv2  11791  ledivdiv  11794  lediv2  11795  ltdiv23  11796  lediv23  11797  sup2  11861  cju  11899  nndivre  11944  nndivtr  11950  nn0addge1  12209  nn0addge2  12210  peano2uz2  12338  uzind  12342  uzind3  12344  fzind  12348  fnn0ind  12349  uzind4  12575  qre  12622  irrmul  12643  rpdivcl  12684  rerpdivcl  12689  xrinfmsslem  12971  ixxin  13025  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  fzaddel  13219  fzadd2  13220  fzrev  13248  modlt  13528  modcyc  13554  axdc4uzlem  13631  expdiv  13762  fundmge2nop0  14134  ccat2s1fvwOLD  14278  swrd00  14285  swrdcl  14286  swrdnnn0nd  14297  swrd0  14299  swrdwrdsymb  14303  ccatpfx  14342  swrdccat  14376  splid  14394  swrdco  14478  2shfti  14719  isermulc2  15297  fsummulc2  15424  dvdscmulr  15922  dvdsmulcr  15923  dvds2add  15927  dvds2sub  15928  dvdstr  15931  alzdvds  15957  divalg2  16042  dvdslegcd  16139  lcmgcdlem  16239  lcmgcdeq  16245  isprm6  16347  pcqcl  16485  vdwmc2  16608  ressinbas  16881  cicer  17435  isposd  17956  pleval2i  17969  poslubmo  18044  posglbmo  18045  tosso  18052  mgmplusf  18251  grprinvd  18273  sgrpidmnd  18305  ismndd  18322  imasmnd2  18337  idmhm  18354  issubm2  18358  0mhm  18373  resmhm  18374  resmhm2  18375  resmhm2b  18376  mhmco  18377  mhmima  18378  submacs  18380  prdspjmhm  18382  pwsdiagmhm  18384  pwsco1mhm  18385  pwsco2mhm  18386  gsumwsubmcl  18390  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  grpinvcnv  18558  grpinvnzcl  18562  grpsubf  18569  imasgrp2  18605  qusgrp2  18608  mhmfmhm  18613  mulgnnsubcl  18631  mulgnndir  18647  issubg4  18689  isnsg3  18703  nsgacs  18705  nsgid  18713  qusadd  18728  ghmmhm  18759  ghmmhmb  18760  idghm  18764  resghm  18765  ghmf1  18778  qusghm  18786  gaid  18820  subgga  18821  gasubg  18823  invoppggim  18882  gsmsymgrfix  18951  smndlsmidm  19176  lsmidmOLD  19184  pj1ghm  19224  mulgnn0di  19342  mulgmhm  19344  mulgghm  19345  ghmfghm  19347  invghm  19350  ghmplusg  19362  ablnsg  19363  qusabl  19381  gsumval3eu  19420  gsumval3  19423  gsumzcl2  19426  gsumzaddlem  19437  gsumzadd  19438  gsumzmhm  19453  gsumzoppg  19460  srgfcl  19666  srgmulgass  19682  srglmhm  19686  srgrmhm  19687  ringlghm  19758  ringrghm  19759  issubrg2  19959  issrngd  20036  islmodd  20044  lmodscaf  20060  lcomf  20077  lmodvsghm  20099  rmodislmodlem  20105  lssacs  20144  idlmhm  20218  invlmhm  20219  lmhmvsca  20222  reslmhm2  20230  reslmhm2b  20231  pwsdiaglmhm  20234  pwssplit2  20237  pwssplit3  20238  issubrngd2  20372  qusrhm  20421  crngridl  20422  quscrng  20424  isnzr2  20447  domnmuln0  20482  opprdomn  20485  expmhm  20579  zntoslem  20676  znfld  20680  psgnghm  20697  phlipf  20769  frlmup1  20915  asclghm  20997  asclrhm  21004  rnasclmulcl  21008  psraddcl  21062  psrvscacl  21072  psrass23  21089  psrbagev1  21195  psrbagev1OLD  21196  coe1sclmulfv  21364  cply1mul  21375  mndvcl  21450  matbas2d  21480  submaeval  21639  minmar1eval  21706  cpmatacl  21773  pmatcollpw1  21833  pmatcollpw  21838  tgclb  22028  topbas  22030  ntrss  22114  mretopd  22151  neissex  22186  cnpnei  22323  lmcnp  22363  ordthaus  22443  llynlly  22536  restnlly  22541  llyidm  22547  nllyidm  22548  ptbasin  22636  txcnp  22679  ist0-4  22788  kqt0lem  22795  isr0  22796  regr1lem2  22799  cmphmph  22847  connhmph  22848  fbun  22899  trfbas2  22902  isfil2  22915  isfild  22917  infil  22922  fbasfip  22927  fbasrn  22943  trfil2  22946  rnelfmlem  23011  fmfnfmlem3  23015  flimopn  23034  txflf  23065  fclsnei  23078  fclsfnflim  23086  fcfnei  23094  clssubg  23168  tgphaus  23176  qustgplem  23180  tsmsadd  23206  psmetxrge0  23374  psmetlecl  23376  xmetlecl  23407  xmettpos  23410  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  elbl3ps  23452  elbl3  23453  metss  23570  comet  23575  stdbdxmet  23577  stdbdmet  23578  methaus  23582  nrmmetd  23636  abvmet  23637  isngp4  23674  subgngp  23697  nmoi2  23800  nmoleub  23801  nmoid  23812  bl2ioo  23861  zcld  23882  divcn  23937  divccn  23942  cncffvrn  23967  divccncf  23975  icoopnst  24008  clmzlmvsca  24182  cph2ass  24282  tcphcph  24306  cfilfcls  24343  bcthlem2  24394  rrxmet  24477  rrxdstprj1  24478  rrxdsfi  24480  cldcss  24510  dvrec  25024  dvmptfsum  25044  aalioulem3  25399  taylply2  25432  efsubm  25612  dchrelbasd  26292  dchrmulcl  26302  2sqreulem3  26506  pntrmax  26617  padicabv  26683  axtgcont  26734  xmstrkgc  27156  axsegconlem1  27188  axlowdimlem15  27227  usgredg2vlem1  27495  usgredg2vlem2  27496  iswlkon  27927  wwlksnextsurj  28166  elwwlks2  28232  elwspths2spth  28233  frrusgrord  28606  numclwwlk1lem2foalem  28616  grpoidinvlem2  28768  grpoidinvlem3  28769  ablo4  28813  ablomuldiv  28815  nvaddsub4  28920  nvmeq0  28921  sspmval  28996  sspimsval  29001  lnosub  29022  dipsubdir  29111  hvadd4  29299  hvpncan  29302  his35  29351  hiassdi  29354  shscli  29580  shmodsi  29652  chj4  29798  spansnmul  29827  spansncol  29831  spanunsni  29842  hoadd4  30047  hosubadd4  30077  lnopl  30177  unopf1o  30179  counop  30184  lnfnl  30194  hmopadj2  30204  eighmre  30226  lnopmi  30263  lnophsi  30264  hmops  30283  hmopm  30284  cnlnadjlem2  30331  adjmul  30355  adjadd  30356  kbass6  30384  mdslj1i  30582  mdslj2i  30583  mdslmd1lem1  30588  mdslmd2i  30593  chirredlem3  30655  isoun  30936  xdivmul  31101  odutos  31148  lmodvslmhm  31212  isarchi2  31341  archiabllem2  31353  quslmhm  31457  tngdim  31598  fedgmullem2  31613  metider  31746  pl1cn  31807  rossros  32048  ismeas  32067  dya2iocnei  32149  inelcarsg  32178  signstfvc  32453  bnj563  32623  fisshasheq  32973  cnpconn  33092  cvmseu  33138  elmrsubrn  33382  mrsubco  33383  nnasmo  33596  ttrclse  33713  nosupbnd2  33846  noinfbnd2  33861  ssltd  33913  fneint  34464  fnessref  34473  tailfb  34493  onsucuni3  35465  pibt2  35515  ptrecube  35704  poimirlem4  35708  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  cnambfre  35752  itg2addnclem2  35756  ftc1anclem5  35781  ftc1anclem6  35782  metf1o  35840  isbnd3b  35870  equivbnd  35875  heiborlem3  35898  rrnmet  35914  rrndstprj1  35915  rrntotbnd  35921  exidcl  35961  ghomco  35976  ghomdiv  35977  grpokerinj  35978  rngoneglmul  36028  rngonegrmul  36029  rngosubdi  36030  rngosubdir  36031  isdrngo2  36043  rngohomco  36059  rngoisocnv  36066  riscer  36073  crngm4  36088  crngohomfo  36091  idlsubcl  36108  inidl  36115  keridl  36117  ispridlc  36155  pridlc3  36158  dmncan1  36161  lflvscl  37018  3dim0  37398  linepsubN  37693  cdlemg2fvlem  38535  trlcoat  38664  istendod  38703  dva1dim  38926  dvhvaddcomN  39037  dihf11  39208  dihlatat  39278  metakunt12  40064  pwspjmhmmgpd  40192  fsuppssind  40205  mhphf  40208  sn-sup2  40360  ismrc  40439  isnacs3  40448  mzpindd  40484  pellex  40573  monotoddzzfi  40680  lermxnn0  40688  rmyeq0  40691  rmyeq  40692  lermy  40693  jm2.27  40746  lsmfgcl  40815  fsumcnsrcl  40907  rngunsnply  40914  isdomn3  40945  gsumws3  41696  mnringmulrcld  41735  nzin  41825  ofdivrec  41833  ofdivcan4  41834  chordthmALT  42442  wessf1ornlem  42611  projf1o  42625  ltdiv23neg  42824  fmulcl  43012  prproropf1olem2  44844  prproropf1olem4  44846  ismgmd  45218  idmgmhm  45230  resmgmhm  45240  resmgmhm2  45241  resmgmhm2b  45242  mgmhmco  45243  mgmhmima  45244  submgmacs  45246  mgmplusgiopALT  45276  c0mgm  45355  c0mhm  45356  itsclc0xyqsolb  46004  toslat  46156