Theorem 3expb 1115

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 1114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 421	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  3expia  1116  3adant3r1  1177  3adant3r2  1178  3adant3r3  1179  mp3an1  1443  sotri  5980  fnfco  6536  mpoeq3dva  7224  oprres  7309  fovrnda  7312  fnmpoovd  7775  offval22  7776  bropfvvvvlem  7779  fnsuppres  7850  suppsssn  7858  sprmpod  7883  oaass  8180  omlimcl  8197  odi  8198  nnmsucr  8244  cflim2  9678  mulcanenq  10375  mul4  10801  add4  10853  2addsub  10893  addsubeq4  10894  subadd4  10923  muladd  11065  ltleadd  11116  divmul  11294  divne0  11303  div23  11310  div12  11313  divsubdir  11327  subdivcomb1  11328  divcan5  11335  divmuleq  11338  divcan6  11340  divdiv32  11341  div2sub  11458  letrp1  11477  lemul12b  11490  lediv1  11498  lt2mul2div  11511  lemuldiv  11513  ltdiv2  11519  ledivdiv  11522  lediv2  11523  ltdiv23  11524  lediv23  11525  sup2  11590  cju  11627  nndivre  11672  nndivtr  11678  nn0addge1  11937  nn0addge2  11938  peano2uz2  12064  uzind  12068  uzind3  12070  fzind  12074  fnn0ind  12075  uzind4  12300  qre  12347  irrmul  12367  rpdivcl  12408  rerpdivcl  12413  xrinfmsslem  12695  ixxin  12749  iccshftr  12868  iccshftl  12870  iccdil  12872  icccntr  12874  fzaddel  12938  fzadd2  12939  fzrev  12967  modlt  13245  modcyc  13271  axdc4uzlem  13348  expdiv  13477  fundmge2nop0  13847  ccat2s1fvwOLD  13994  swrd00  14001  swrdcl  14002  swrdnnn0nd  14013  swrd0  14015  swrdwrdsymb  14019  ccatpfx  14058  swrdccat  14092  splid  14110  swrdco  14194  2shfti  14434  isermulc2  15009  fsummulc2  15134  dvdscmulr  15633  dvdsmulcr  15634  dvds2add  15638  dvds2sub  15639  dvdstr  15641  alzdvds  15665  divalg2  15751  dvdslegcd  15848  lcmgcdlem  15945  lcmgcdeq  15951  isprm6  16053  pcqcl  16188  vdwmc2  16310  ressinbas  16555  cicer  17071  isposd  17560  pleval2i  17569  tosso  17641  poslubmo  17751  posglbmo  17752  mgmplusf  17857  grprinvd  17879  sgrpidmnd  17911  ismndd  17928  imasmnd2  17943  idmhm  17960  issubm2  17964  0mhm  17979  resmhm  17980  resmhm2  17981  resmhm2b  17982  mhmco  17983  mhmima  17984  submacs  17986  prdspjmhm  17988  pwsdiagmhm  17990  pwsco1mhm  17991  pwsco2mhm  17992  gsumwsubmcl  17996  gsumsgrpccat  17999  gsumccatOLD  18000  gsumwmhm  18005  grpinvcnv  18162  grpinvnzcl  18166  grpsubf  18173  imasgrp2  18209  qusgrp2  18212  mhmfmhm  18217  mulgnnsubcl  18235  mulgnndir  18251  issubg4  18293  isnsg3  18307  nsgacs  18309  nsgid  18317  qusadd  18332  ghmmhm  18363  ghmmhmb  18364  idghm  18368  resghm  18369  ghmf1  18382  qusghm  18390  gaid  18424  subgga  18425  gasubg  18427  invoppggim  18483  gsmsymgrfix  18551  smndlsmidm  18776  lsmidmOLD  18784  pj1ghm  18824  mulgnn0di  18941  mulgmhm  18943  mulgghm  18944  ghmfghm  18946  invghm  18949  ghmplusg  18961  ablnsg  18962  qusabl  18980  gsumval3eu  19019  gsumval3  19022  gsumzcl2  19025  gsumzaddlem  19036  gsumzadd  19037  gsumzmhm  19052  gsumzoppg  19059  srgfcl  19260  srgmulgass  19276  srglmhm  19280  srgrmhm  19281  ringlghm  19349  ringrghm  19350  issubrg2  19550  issrngd  19627  islmodd  19635  lmodscaf  19651  lcomf  19668  lmodvsghm  19690  rmodislmodlem  19696  lssacs  19734  idlmhm  19808  invlmhm  19809  lmhmvsca  19812  reslmhm2  19820  reslmhm2b  19821  pwsdiaglmhm  19824  pwssplit2  19827  pwssplit3  19828  issubrngd2  19956  qusrhm  20005  crngridl  20006  quscrng  20008  isnzr2  20031  domnmuln0  20066  opprdomn  20069  asclghm  20107  asclrhm  20114  rnasclmulcl  20118  psraddcl  20158  psrvscacl  20168  psrass23  20185  psrbagev1  20285  coe1sclmulfv  20446  cply1mul  20457  expmhm  20609  zntoslem  20698  znfld  20702  psgnghm  20719  phlipf  20791  frlmup1  20937  mndvcl  20997  matbas2d  21027  submaeval  21186  minmar1eval  21253  cpmatacl  21319  pmatcollpw1  21379  pmatcollpw  21384  tgclb  21573  topbas  21575  ntrss  21658  mretopd  21695  neissex  21730  cnpnei  21867  lmcnp  21907  ordthaus  21987  llynlly  22080  restnlly  22085  llyidm  22091  nllyidm  22092  ptbasin  22180  txcnp  22223  ist0-4  22332  kqt0lem  22339  isr0  22340  regr1lem2  22343  cmphmph  22391  connhmph  22392  fbun  22443  trfbas2  22446  isfil2  22459  isfild  22461  infil  22466  fbasfip  22471  fbasrn  22487  trfil2  22490  rnelfmlem  22555  fmfnfmlem3  22559  flimopn  22578  txflf  22609  fclsnei  22622  fclsfnflim  22630  fcfnei  22638  clssubg  22712  tgphaus  22720  qustgplem  22724  tsmsadd  22750  psmetxrge0  22918  psmetlecl  22920  xmetlecl  22951  xmettpos  22954  imasdsf1olem  22978  imasf1oxmet  22980  imasf1omet  22981  elbl3ps  22996  elbl3  22997  metss  23113  comet  23118  stdbdxmet  23120  stdbdmet  23121  methaus  23125  nrmmetd  23179  abvmet  23180  isngp4  23216  subgngp  23239  nmoi2  23334  nmoleub  23335  nmoid  23346  bl2ioo  23395  zcld  23416  divcn  23471  divccn  23476  cncffvrn  23501  divccncf  23509  icoopnst  23538  clmzlmvsca  23712  cph2ass  23812  tcphcph  23835  cfilfcls  23872  bcthlem2  23923  rrxmet  24006  rrxdstprj1  24007  rrxdsfi  24009  cldcss  24039  dvrec  24549  dvmptfsum  24569  aalioulem3  24921  taylply2  24954  efsubm  25133  dchrelbasd  25813  dchrmulcl  25823  2sqreulem3  26027  pntrmax  26138  padicabv  26204  axtgcont  26253  xmstrkgc  26670  axsegconlem1  26701  axlowdimlem15  26740  usgredg2vlem1  27005  usgredg2vlem2  27006  iswlkon  27437  wwlksnextsurj  27676  elwwlks2  27743  elwspths2spth  27744  frrusgrord  28118  numclwwlk1lem2foalem  28128  grpoidinvlem2  28280  grpoidinvlem3  28281  ablo4  28325  ablomuldiv  28327  nvaddsub4  28432  nvmeq0  28433  sspmval  28508  sspimsval  28513  lnosub  28534  dipsubdir  28623  hvadd4  28811  hvpncan  28814  his35  28863  hiassdi  28866  shscli  29092  shmodsi  29164  chj4  29310  spansnmul  29339  spansncol  29343  spanunsni  29354  hoadd4  29559  hosubadd4  29589  lnopl  29689  unopf1o  29691  counop  29696  lnfnl  29706  hmopadj2  29716  eighmre  29738  lnopmi  29775  lnophsi  29776  hmops  29795  hmopm  29796  cnlnadjlem2  29843  adjmul  29867  adjadd  29868  kbass6  29896  mdslj1i  30094  mdslj2i  30095  mdslmd1lem1  30100  mdslmd2i  30105  chirredlem3  30167  isoun  30437  xdivmul  30601  odutos  30650  lmodvslmhm  30709  isarchi2  30835  archiabllem2  30847  quslmhm  30945  tngdim  31035  fedgmullem2  31050  metider  31158  pl1cn  31219  rossros  31460  ismeas  31479  dya2iocnei  31561  inelcarsg  31590  signstfvc  31865  bnj563  32035  fisshasheq  32373  cnpconn  32498  cvmseu  32544  elmrsubrn  32788  mrsubco  32789  nosupbnd2  33237  fneint  33717  fnessref  33726  tailfb  33746  onsucuni3  34672  pibt2  34722  ptrecube  34927  poimirlem4  34931  heicant  34962  mblfinlem1  34964  mblfinlem2  34965  mblfinlem3  34966  mblfinlem4  34967  cnambfre  34975  itg2addnclem2  34979  ftc1anclem5  35004  ftc1anclem6  35005  metf1o  35063  isbnd3b  35096  equivbnd  35101  heiborlem3  35124  rrnmet  35140  rrndstprj1  35141  rrntotbnd  35147  exidcl  35187  ghomco  35202  ghomdiv  35203  grpokerinj  35204  rngoneglmul  35254  rngonegrmul  35255  rngosubdi  35256  rngosubdir  35257  isdrngo2  35269  rngohomco  35285  rngoisocnv  35292  riscer  35299  crngm4  35314  crngohomfo  35317  idlsubcl  35334  inidl  35341  keridl  35343  ispridlc  35381  pridlc3  35384  dmncan1  35387  lflvscl  36246  3dim0  36626  linepsubN  36921  cdlemg2fvlem  37763  trlcoat  37892  istendod  37931  dva1dim  38154  dvhvaddcomN  38265  dihf11  38436  dihlatat  38506  ismrc  39374  isnacs3  39383  mzpindd  39419  pellex  39508  monotoddzzfi  39615  lermxnn0  39623  rmyeq0  39626  rmyeq  39627  lermy  39628  jm2.27  39681  lsmfgcl  39750  fsumcnsrcl  39842  rngunsnply  39849  isdomn3  39880  gsumws3  40623  nzin  40724  ofdivrec  40732  ofdivcan4  40733  chordthmALT  41341  wessf1ornlem  41519  projf1o  41533  ltdiv23neg  41740  fmulcl  41936  prproropf1olem2  43740  prproropf1olem4  43742  ismgmd  44117  idmgmhm  44129  resmgmhm  44139  resmgmhm2  44140  resmgmhm2b  44141  mgmhmco  44142  mgmhmima  44143  submgmacs  44145  mgmplusgiopALT  44175  c0mgm  44254  c0mhm  44255  itsclc0xyqsolb  44831