Theorem 3expb 1120

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

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

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 1088

This theorem is referenced by:  3expia  1121  3adant3r1  1183  3adant3r2  1184  3adant3r3  1185  mp3an1  1450  sotri  6100  fnfco  6725  mpoeq3dva  7466  oprres  7557  fovcdmda  7560  fnmpoovd  8066  offval22  8067  bropfvvvvlem  8070  fnsuppres  8170  suppsssn  8180  sprmpod  8203  oaass  8525  omlimcl  8542  odi  8543  nnmsucr  8589  nnasmo  8627  unfi  9135  ttrclse  9680  cflim2  10216  mulcanenq  10913  mul4  11342  add4  11395  2addsub  11435  addsubeq4  11436  subadd4  11466  muladd  11610  ltleadd  11661  divmul  11840  divne0  11849  div23  11856  div12  11859  div11  11865  divsubdir  11876  subdivcomb1  11877  divcan5  11884  divmuleq  11887  divcan6  11889  divdiv32  11890  div2sub  12007  letrp1  12026  lemul12b  12039  lediv1  12048  lt2mul2div  12061  lemuldiv  12063  ltdiv2  12069  ledivdiv  12072  lediv2  12073  ltdiv23  12074  lediv23  12075  sup2  12139  cju  12182  nndivre  12227  nndivtr  12233  nn0addge1  12488  nn0addge2  12489  peano2uz2  12622  uzind  12626  uzind3  12628  fzind  12632  fnn0ind  12633  uzind4  12865  qre  12912  irrmul  12933  rpdivcl  12978  rerpdivcl  12983  xrinfmsslem  13268  ixxin  13323  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzaddel  13519  fzadd2  13520  fzrev  13548  modlt  13842  modcyc  13868  axdc4uzlem  13948  expdiv  14078  fundmge2nop0  14467  swrd00  14609  swrdcl  14610  swrdnnn0nd  14621  swrd0  14623  swrdwrdsymb  14627  ccatpfx  14666  swrdccat  14700  splid  14718  swrdco  14803  2shfti  15046  isermulc2  15624  fsummulc2  15750  dvdscmulr  16254  dvdsmulcr  16255  dvds2add  16260  dvds2sub  16261  dvdstr  16264  alzdvds  16290  divalg2  16375  dvdslegcd  16474  lcmgcdlem  16576  lcmgcdeq  16582  isprm6  16684  pcqcl  16827  vdwmc2  16950  ressinbas  17215  cicer  17768  isposd  18283  pleval2i  18295  poslubmo  18370  posglbmo  18371  tosso  18378  mgmplusf  18577  ismgmd  18579  grpinva  18601  idmgmhm  18628  resmgmhm  18638  resmgmhm2  18639  resmgmhm2b  18640  mgmhmco  18641  mgmhmima  18642  submgmacs  18644  sgrpidmnd  18666  ismndd  18683  imasmnd2  18701  idmhm  18722  mndvcl  18724  issubm2  18731  0mhm  18746  resmhm  18747  resmhm2  18748  resmhm2b  18749  mhmco  18750  mhmimalem  18751  submacs  18754  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  grpinvcnv  18938  grpinvnzcl  18943  grpsubf  18951  imasgrp2  18987  qusgrp2  18990  mhmfmhm  18997  mulgnnsubcl  19018  mulgnndir  19035  issubg4  19077  isnsg3  19092  nsgacs  19094  nsgid  19102  qusadd  19120  qus0subgadd  19131  ghmmhm  19158  ghmmhmb  19159  idghm  19163  resghm  19164  ghmf1  19178  qusghm  19187  gaid  19231  subgga  19232  gasubg  19234  invoppggim  19292  gsmsymgrfix  19358  smndlsmidm  19586  pj1ghm  19633  mulgnn0di  19755  mulgmhm  19757  mulgghm  19758  ghmfghm  19760  invghm  19763  ghmplusg  19776  ablnsg  19777  qusabl  19795  gsumval3eu  19834  gsumval3  19837  gsumzcl2  19840  gsumzaddlem  19851  gsumzadd  19852  gsumzmhm  19867  gsumzoppg  19874  srgfcl  20105  srgcom4lem  20122  srgmulgass  20126  srglmhm  20130  srgrmhm  20131  ringcomlem  20188  ringlghm  20221  ringrghm  20222  pwspjmhmmgpd  20237  c0mgm  20368  c0mhm  20369  isnzr2  20427  subrngringnsg  20462  issubrng2  20467  rhmimasubrnglem  20474  issubrg2  20501  domnmuln0  20618  isdomn3  20624  issrngd  20764  islmodd  20772  lmodscaf  20790  lcomf  20807  lmodvsghm  20829  rmodislmodlem  20835  lssacs  20873  idlmhm  20948  invlmhm  20949  lmhmvsca  20952  reslmhm2  20960  reslmhm2b  20961  pwsdiaglmhm  20964  pwssplit2  20967  pwssplit3  20968  issubrgd  21096  qusrhm  21186  qusmul2idl  21189  crngridl  21190  qusmulrng  21192  expmhm  21353  zntoslem  21466  znfld  21470  psgnghm  21489  phlipf  21561  frlmup1  21707  asclghm  21792  asclrhm  21799  rnasclmulcl  21803  psraddcl  21847  psraddclOLD  21848  psrvscacl  21860  psrass23  21878  psrbagev1  21984  coe1sclmulfv  22169  cply1mul  22183  evls1fpws  22256  rhmply1vsca  22275  matbas2d  22310  submaeval  22469  minmar1eval  22536  cpmatacl  22603  pmatcollpw1  22663  pmatcollpw  22668  tgclb  22857  topbas  22859  ntrss  22942  mretopd  22979  neissex  23014  cnpnei  23151  lmcnp  23191  ordthaus  23271  llynlly  23364  restnlly  23369  llyidm  23375  nllyidm  23376  ptbasin  23464  txcnp  23507  ist0-4  23616  kqt0lem  23623  isr0  23624  regr1lem2  23627  cmphmph  23675  connhmph  23676  fbun  23727  trfbas2  23730  isfil2  23743  isfild  23745  infil  23750  fbasfip  23755  fbasrn  23771  trfil2  23774  rnelfmlem  23839  fmfnfmlem3  23843  flimopn  23862  txflf  23893  fclsnei  23906  fclsfnflim  23914  fcfnei  23922  clssubg  23996  tgphaus  24004  qustgplem  24008  tsmsadd  24034  psmetxrge0  24201  psmetlecl  24203  xmetlecl  24234  xmettpos  24237  imasdsf1olem  24261  imasf1oxmet  24263  imasf1omet  24264  elbl3ps  24279  elbl3  24280  metss  24396  comet  24401  stdbdxmet  24403  stdbdmet  24404  methaus  24408  nrmmetd  24462  abvmet  24463  isngp4  24500  subgngp  24523  nmoi2  24618  nmoleub  24619  nmoid  24630  bl2ioo  24680  zcld  24702  divcnOLD  24757  divcn  24759  divccn  24764  divccnOLD  24766  cncfcdm  24791  divccncf  24799  icoopnst  24836  clmzlmvsca  25013  cph2ass  25113  tcphcph  25137  cfilfcls  25174  bcthlem2  25225  rrxmet  25308  rrxdstprj1  25309  rrxdsfi  25311  cldcss  25341  dvrec  25859  dvmptfsum  25879  aalioulem3  26242  taylply2  26275  taylply2OLD  26276  efsubm  26460  dchrelbasd  27150  dchrmulcl  27160  2sqreulem3  27364  pntrmax  27475  padicabv  27541  nosupbnd2  27628  noinfbnd2  27643  ssltd  27703  divsmulw  28096  axtgcont  28396  xmstrkgc  28813  axsegconlem1  28844  axlowdimlem15  28883  usgredg2vlem1  29152  usgredg2vlem2  29153  iswlkon  29585  wwlksnextsurj  29830  elwwlks2  29896  elwspths2spth  29897  frrusgrord  30270  numclwwlk1lem2foalem  30280  grpoidinvlem2  30434  grpoidinvlem3  30435  ablo4  30479  ablomuldiv  30481  nvaddsub4  30586  nvmeq0  30587  sspmval  30662  sspimsval  30667  lnosub  30688  dipsubdir  30777  hvadd4  30965  hvpncan  30968  his35  31017  hiassdi  31020  shscli  31246  shmodsi  31318  chj4  31464  spansnmul  31493  spansncol  31497  spanunsni  31508  hoadd4  31713  hosubadd4  31743  lnopl  31843  unopf1o  31845  counop  31850  lnfnl  31860  hmopadj2  31870  eighmre  31892  lnopmi  31929  lnophsi  31930  hmops  31949  hmopm  31950  cnlnadjlem2  31997  adjmul  32021  adjadd  32022  kbass6  32050  mdslj1i  32248  mdslj2i  32249  mdslmd1lem1  32254  mdslmd2i  32259  chirredlem3  32321  isoun  32625  xdivmul  32845  odutos  32894  lmodvslmhm  32990  isarchi2  33139  archiabllem2  33151  imasmhm  33325  imasghm  33326  imasrhm  33327  imaslmhm  33328  quslmhm  33330  tngdim  33609  fedgmullem2  33626  metider  33884  pl1cn  33945  rossros  34170  ismeas  34189  dya2iocnei  34273  inelcarsg  34302  signstfvc  34565  bnj563  34733  fisshasheq  35102  cnpconn  35217  cvmseu  35263  elmrsubrn  35507  mrsubco  35508  fneint  36336  fnessref  36345  tailfb  36365  onsucuni3  37355  pibt2  37405  ptrecube  37614  poimirlem4  37618  heicant  37649  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  cnambfre  37662  itg2addnclem2  37666  ftc1anclem5  37691  ftc1anclem6  37692  metf1o  37749  isbnd3b  37779  equivbnd  37784  heiborlem3  37807  rrnmet  37823  rrndstprj1  37824  rrntotbnd  37830  exidcl  37870  ghomco  37885  ghomdiv  37886  grpokerinj  37887  rngoneglmul  37937  rngonegrmul  37938  rngosubdi  37939  rngosubdir  37940  isdrngo2  37952  rngohomco  37968  rngoisocnv  37975  riscer  37982  crngm4  37997  crngohomfo  38000  idlsubcl  38017  inidl  38024  keridl  38026  ispridlc  38064  pridlc3  38067  dmncan1  38070  lflvscl  39070  3dim0  39451  linepsubN  39746  cdlemg2fvlem  40588  trlcoat  40717  istendod  40756  dva1dim  40979  dvhvaddcomN  41090  dihf11  41261  dihlatat  41331  sn-sup2  42479  fsuppssind  42581  mhphf  42585  ismrc  42689  isnacs3  42698  mzpindd  42734  pellex  42823  monotoddzzfi  42931  lermxnn0  42939  rmyeq0  42942  rmyeq  42943  lermy  42944  jm2.27  42997  lsmfgcl  43063  fsumcnsrcl  43155  rngunsnply  43158  gsumws3  44185  mnringmulrcld  44217  nzin  44307  ofdivrec  44315  ofdivcan4  44316  chordthmALT  44922  wessf1ornlem  45179  projf1o  45191  ltdiv23neg  45390  fmulcl  45579  prproropf1olem2  47505  prproropf1olem4  47507  mgmplusgiopALT  48182  itsclc0xyqsolb  48759  toslat  48970  cicerALT  49035