Theorem 3expb 1119

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3expia  1120  3adant3r1  1181  3adant3r2  1182  3adant3r3  1183  mp3an1  1447  sotri  6037  fnfco  6648  mpoeq3dva  7361  oprres  7449  fovrnda  7452  fnmpoovd  7936  offval22  7937  bropfvvvvlem  7940  fnsuppres  8016  suppsssn  8026  sprmpod  8049  oaass  8401  omlimcl  8418  odi  8419  nnmsucr  8465  nnasmo  8502  unfi  8964  ttrclse  9494  cflim2  10028  mulcanenq  10725  mul4  11152  add4  11204  2addsub  11244  addsubeq4  11245  subadd4  11274  muladd  11416  ltleadd  11467  divmul  11645  divne0  11654  div23  11661  div12  11664  divsubdir  11678  subdivcomb1  11679  divcan5  11686  divmuleq  11689  divcan6  11691  divdiv32  11692  div2sub  11809  letrp1  11828  lemul12b  11841  lediv1  11849  lt2mul2div  11862  lemuldiv  11864  ltdiv2  11870  ledivdiv  11873  lediv2  11874  ltdiv23  11875  lediv23  11876  sup2  11940  cju  11978  nndivre  12023  nndivtr  12029  nn0addge1  12288  nn0addge2  12289  peano2uz2  12417  uzind  12421  uzind3  12423  fzind  12427  fnn0ind  12428  uzind4  12655  qre  12702  irrmul  12723  rpdivcl  12764  rerpdivcl  12769  xrinfmsslem  13051  ixxin  13105  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  fzaddel  13299  fzadd2  13300  fzrev  13328  modlt  13609  modcyc  13635  axdc4uzlem  13712  expdiv  13843  fundmge2nop0  14215  ccat2s1fvwOLD  14359  swrd00  14366  swrdcl  14367  swrdnnn0nd  14378  swrd0  14380  swrdwrdsymb  14384  ccatpfx  14423  swrdccat  14457  splid  14475  swrdco  14559  2shfti  14800  isermulc2  15378  fsummulc2  15505  dvdscmulr  16003  dvdsmulcr  16004  dvds2add  16008  dvds2sub  16009  dvdstr  16012  alzdvds  16038  divalg2  16123  dvdslegcd  16220  lcmgcdlem  16320  lcmgcdeq  16326  isprm6  16428  pcqcl  16566  vdwmc2  16689  ressinbas  16964  cicer  17527  isposd  18050  pleval2i  18063  poslubmo  18138  posglbmo  18139  tosso  18146  mgmplusf  18345  grprinvd  18367  sgrpidmnd  18399  ismndd  18416  imasmnd2  18431  idmhm  18448  issubm2  18452  0mhm  18467  resmhm  18468  resmhm2  18469  resmhm2b  18470  mhmco  18471  mhmima  18472  submacs  18474  prdspjmhm  18476  pwsdiagmhm  18478  pwsco1mhm  18479  pwsco2mhm  18480  gsumwsubmcl  18484  gsumsgrpccat  18487  gsumccatOLD  18488  gsumwmhm  18493  grpinvcnv  18652  grpinvnzcl  18656  grpsubf  18663  imasgrp2  18699  qusgrp2  18702  mhmfmhm  18707  mulgnnsubcl  18725  mulgnndir  18741  issubg4  18783  isnsg3  18797  nsgacs  18799  nsgid  18807  qusadd  18822  ghmmhm  18853  ghmmhmb  18854  idghm  18858  resghm  18859  ghmf1  18872  qusghm  18880  gaid  18914  subgga  18915  gasubg  18917  invoppggim  18976  gsmsymgrfix  19045  smndlsmidm  19270  lsmidmOLD  19278  pj1ghm  19318  mulgnn0di  19436  mulgmhm  19438  mulgghm  19439  ghmfghm  19441  invghm  19444  ghmplusg  19456  ablnsg  19457  qusabl  19475  gsumval3eu  19514  gsumval3  19517  gsumzcl2  19520  gsumzaddlem  19531  gsumzadd  19532  gsumzmhm  19547  gsumzoppg  19554  srgfcl  19760  srgmulgass  19776  srglmhm  19780  srgrmhm  19781  ringlghm  19852  ringrghm  19853  issubrg2  20053  issrngd  20130  islmodd  20138  lmodscaf  20154  lcomf  20171  lmodvsghm  20193  rmodislmodlem  20199  lssacs  20238  idlmhm  20312  invlmhm  20313  lmhmvsca  20316  reslmhm2  20324  reslmhm2b  20325  pwsdiaglmhm  20328  pwssplit2  20331  pwssplit3  20332  issubrngd2  20468  qusrhm  20517  crngridl  20518  quscrng  20520  isnzr2  20543  domnmuln0  20578  opprdomn  20581  expmhm  20676  zntoslem  20773  znfld  20777  psgnghm  20794  phlipf  20866  frlmup1  21014  asclghm  21096  asclrhm  21103  rnasclmulcl  21107  psraddcl  21161  psrvscacl  21171  psrass23  21188  psrbagev1  21294  psrbagev1OLD  21295  coe1sclmulfv  21463  cply1mul  21474  mndvcl  21549  matbas2d  21581  submaeval  21740  minmar1eval  21807  cpmatacl  21874  pmatcollpw1  21934  pmatcollpw  21939  tgclb  22129  topbas  22131  ntrss  22215  mretopd  22252  neissex  22287  cnpnei  22424  lmcnp  22464  ordthaus  22544  llynlly  22637  restnlly  22642  llyidm  22648  nllyidm  22649  ptbasin  22737  txcnp  22780  ist0-4  22889  kqt0lem  22896  isr0  22897  regr1lem2  22900  cmphmph  22948  connhmph  22949  fbun  23000  trfbas2  23003  isfil2  23016  isfild  23018  infil  23023  fbasfip  23028  fbasrn  23044  trfil2  23047  rnelfmlem  23112  fmfnfmlem3  23116  flimopn  23135  txflf  23166  fclsnei  23179  fclsfnflim  23187  fcfnei  23195  clssubg  23269  tgphaus  23277  qustgplem  23281  tsmsadd  23307  psmetxrge0  23475  psmetlecl  23477  xmetlecl  23508  xmettpos  23511  imasdsf1olem  23535  imasf1oxmet  23537  imasf1omet  23538  elbl3ps  23553  elbl3  23554  metss  23673  comet  23678  stdbdxmet  23680  stdbdmet  23681  methaus  23685  nrmmetd  23739  abvmet  23740  isngp4  23777  subgngp  23800  nmoi2  23903  nmoleub  23904  nmoid  23915  bl2ioo  23964  zcld  23985  divcn  24040  divccn  24045  cncffvrn  24070  divccncf  24078  icoopnst  24111  clmzlmvsca  24285  cph2ass  24386  tcphcph  24410  cfilfcls  24447  bcthlem2  24498  rrxmet  24581  rrxdstprj1  24582  rrxdsfi  24584  cldcss  24614  dvrec  25128  dvmptfsum  25148  aalioulem3  25503  taylply2  25536  efsubm  25716  dchrelbasd  26396  dchrmulcl  26406  2sqreulem3  26610  pntrmax  26721  padicabv  26787  axtgcont  26839  xmstrkgc  27262  axsegconlem1  27294  axlowdimlem15  27333  usgredg2vlem1  27601  usgredg2vlem2  27602  iswlkon  28034  wwlksnextsurj  28274  elwwlks2  28340  elwspths2spth  28341  frrusgrord  28714  numclwwlk1lem2foalem  28724  grpoidinvlem2  28876  grpoidinvlem3  28877  ablo4  28921  ablomuldiv  28923  nvaddsub4  29028  nvmeq0  29029  sspmval  29104  sspimsval  29109  lnosub  29130  dipsubdir  29219  hvadd4  29407  hvpncan  29410  his35  29459  hiassdi  29462  shscli  29688  shmodsi  29760  chj4  29906  spansnmul  29935  spansncol  29939  spanunsni  29950  hoadd4  30155  hosubadd4  30185  lnopl  30285  unopf1o  30287  counop  30292  lnfnl  30302  hmopadj2  30312  eighmre  30334  lnopmi  30371  lnophsi  30372  hmops  30391  hmopm  30392  cnlnadjlem2  30439  adjmul  30463  adjadd  30464  kbass6  30492  mdslj1i  30690  mdslj2i  30691  mdslmd1lem1  30696  mdslmd2i  30701  chirredlem3  30763  isoun  31043  xdivmul  31208  odutos  31255  lmodvslmhm  31319  isarchi2  31448  archiabllem2  31460  quslmhm  31564  tngdim  31705  fedgmullem2  31720  metider  31853  pl1cn  31914  rossros  32157  ismeas  32176  dya2iocnei  32258  inelcarsg  32287  signstfvc  32562  bnj563  32732  fisshasheq  33082  cnpconn  33201  cvmseu  33247  elmrsubrn  33491  mrsubco  33492  nosupbnd2  33928  noinfbnd2  33943  ssltd  33995  fneint  34546  fnessref  34555  tailfb  34575  onsucuni3  35547  pibt2  35597  ptrecube  35786  poimirlem4  35790  heicant  35821  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  cnambfre  35834  itg2addnclem2  35838  ftc1anclem5  35863  ftc1anclem6  35864  metf1o  35922  isbnd3b  35952  equivbnd  35957  heiborlem3  35980  rrnmet  35996  rrndstprj1  35997  rrntotbnd  36003  exidcl  36043  ghomco  36058  ghomdiv  36059  grpokerinj  36060  rngoneglmul  36110  rngonegrmul  36111  rngosubdi  36112  rngosubdir  36113  isdrngo2  36125  rngohomco  36141  rngoisocnv  36148  riscer  36155  crngm4  36170  crngohomfo  36173  idlsubcl  36190  inidl  36197  keridl  36199  ispridlc  36237  pridlc3  36240  dmncan1  36243  lflvscl  37098  3dim0  37478  linepsubN  37773  cdlemg2fvlem  38615  trlcoat  38744  istendod  38783  dva1dim  39006  dvhvaddcomN  39117  dihf11  39288  dihlatat  39358  metakunt12  40143  pwspjmhmmgpd  40274  fsuppssind  40289  mhphf  40292  sn-sup2  40446  ismrc  40530  isnacs3  40539  mzpindd  40575  pellex  40664  monotoddzzfi  40771  lermxnn0  40779  rmyeq0  40782  rmyeq  40783  lermy  40784  jm2.27  40837  lsmfgcl  40906  fsumcnsrcl  40998  rngunsnply  41005  isdomn3  41036  gsumws3  41814  mnringmulrcld  41853  nzin  41943  ofdivrec  41951  ofdivcan4  41952  chordthmALT  42560  wessf1ornlem  42729  projf1o  42743  ltdiv23neg  42941  fmulcl  43129  prproropf1olem2  44967  prproropf1olem4  44969  ismgmd  45341  idmgmhm  45353  resmgmhm  45363  resmgmhm2  45364  resmgmhm2b  45365  mgmhmco  45366  mgmhmima  45367  submgmacs  45369  mgmplusgiopALT  45399  c0mgm  45478  c0mhm  45479  itsclc0xyqsolb  46127  toslat  46279