Theorem 3expb 1138

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3expia  1139  3adant3r1  1201  3adant3r2  1202  3adant3r3  1203  mp3an1  1477  sotri  6127  fnfco  6743  mpoeq3dva  7487  oprres  7578  fovcdmda  7581  fnmpoovd  8078  offval22  8079  bropfvvvvlem  8082  fnsuppres  8183  suppsssn  8193  sprmpod  8216  oaass  8542  omlimcl  8559  odi  8560  nnmsucr  8607  nnasmo  8645  unfi  9151  ttrclse  9692  cflim2  10242  mulcanenq  10940  mul4  11373  add4  11426  2addsub  11466  addsubeq4  11467  subadd4  11497  muladd  11641  ltleadd  11692  divmul  11870  divne0  11879  div23  11886  div12  11889  div11  11895  divsubdir  11903  subdivcomb1  11905  divcan5  11912  divmuleq  11915  divcan6  11917  divdiv32  11918  div2sub  12035  letrp1  12054  lemul12b  12067  lediv1  12075  lt2mul2div  12088  lemuldiv  12090  ltdiv2  12096  ledivdiv  12099  lediv2  12100  ltdiv23  12101  lediv23  12102  sup2  12166  cju  12209  nndivre  12272  nndivtr  12278  nn0addge1  12545  nn0addge2  12546  peano2uz2  12679  uzind  12683  uzind3  12685  fzind  12689  fnn0ind  12690  uzind4  12925  qre  12972  irrmul  12993  rpdivcl  13038  rerpdivcl  13043  xrinfmsslem  13329  ixxin  13384  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  fzaddel  13582  fzadd2  13583  fzrev  13611  modlt  13909  modcyc  13935  axdc4uzlem  14015  expdiv  14145  fundmge2nop0  14535  swrd00  14678  swrdcl  14679  swrdnnn0nd  14690  swrd0  14692  swrdwrdsymb  14696  ccatpfx  14734  swrdccat  14768  splid  14786  swrdco  14870  2shfti  15113  isermulc2  15705  fsummulc2  15831  dvdscmulr  16337  dvdsmulcr  16338  dvds2add  16343  dvds2sub  16344  dvdstr  16347  alzdvds  16373  divalg2  16458  dvdslegcd  16557  lcmgcdlem  16659  lcmgcdeq  16665  isprm6  16768  pcqcl  16911  vdwmc2  17034  ressinbas  17300  cicer  17858  isposd  18373  pleval2i  18385  poslubmo  18460  posglbmo  18461  tosso  18468  mgmplusf  18703  ismgmd  18705  grpinva  18727  idmgmhm  18754  resmgmhm  18764  resmgmhm2  18765  resmgmhm2b  18766  mgmhmco  18767  mgmhmima  18768  submgmacs  18770  sgrpidmnd  18792  ismndd  18809  imasmnd2  18827  idmhm  18848  mndvcl  18850  issubm2  18857  0mhm  18873  resmhm  18874  resmhm2  18875  resmhm2b  18876  mhmco  18877  mhmimalem  18878  submacs  18881  prdspjmhm  18883  pwsdiagmhm  18885  pwsco1mhm  18886  pwsco2mhm  18887  gsumwsubmcl  18891  gsumsgrpccat  18894  gsumwmhm  18899  grpinvcnv  19068  grpinvnzcl  19072  grpsubf  19080  imasgrp2  19116  qusgrp2  19119  mhmfmhm  19126  mulgnnsubcl  19147  mulgnndir  19164  issubg4  19207  isnsg3  19221  nsgacs  19223  nsgid  19231  qusadd  19254  qus0subgadd  19265  ghmmhm  19291  ghmmhmb  19292  idghm  19296  resghm  19297  ghmf1  19311  qusghm  19320  gaid  19364  subgga  19365  gasubg  19367  invoppggim  19425  gsmsymgrfix  19493  smndlsmidm  19721  pj1ghm  19768  mulgnn0di  19890  mulgmhm  19892  mulgghm  19893  ghmfghm  19895  invghm  19898  ghmplusg  19911  ablnsg  19912  qusabl  19930  gsumval3eu  19969  gsumval3  19972  gsumzcl2  19975  gsumzaddlem  19986  gsumzadd  19987  gsumzmhm  20002  gsumzoppg  20009  srgfcl  20273  srgcom4lem  20290  srgmulgass  20294  srglmhm  20298  srgrmhm  20299  ringcomlem  20358  ringlghm  20391  ringrghm  20392  pwspjmhmmgpd  20405  c0mgm  20537  c0mhm  20538  isnzr2  20615  subrngringnsg  20652  issubrng2  20657  rhmimasubrnglem  20664  issubrg2  20691  domnmuln0  20808  isdomn3  20813  isdrng3lem2  20852  issrngd  20958  islmodd  20987  lmodscaf  21005  lcomf  21022  lmodvsghm  21044  rmodislmodlem  21050  lssacs  21088  idlmhm  21162  invlmhm  21163  lmhmvsca  21166  reslmhm2  21174  reslmhm2b  21175  pwsdiaglmhm  21178  pwssplit2  21181  pwssplit3  21182  issubrgd  21310  qusrhm  21415  qusmul2idl  21418  crngridl  21419  qusmulrng  21422  cmprmidlmcl  21475  expmhm  21586  zntoslem  21706  znfld  21710  psgnghm  21730  phlipf  21802  frlmup1  21948  asclghm  22032  asclrhm  22040  rnasclmulcl  22044  psraddcl  22089  psrvscacl  22101  psrass23  22118  psrbagev1  22228  coe1sclmulfv  22444  cply1mul  22456  evls1fpws  22529  rhmply1vsca  22545  matbas2d  22580  submaeval  22739  minmar1eval  22806  cpmatacl  22873  pmatcollpw1  22933  pmatcollpw  22938  tgclb  23127  topbas  23129  ntrss  23212  mretopd  23249  neissex  23284  cnpnei  23421  lmcnp  23461  ordthaus  23541  llynlly  23634  restnlly  23639  llyidm  23645  nllyidm  23646  ptbasin  23734  txcnp  23777  ist0-4  23886  kqt0lem  23893  isr0  23894  regr1lem2  23897  cmphmph  23945  connhmph  23946  fbun  23997  trfbas2  24000  isfil2  24013  isfild  24015  infil  24020  fbasfip  24025  fbasrn  24041  trfil2  24044  rnelfmlem  24109  fmfnfmlem3  24113  flimopn  24132  txflf  24163  fclsnei  24176  fclsfnflim  24184  fcfnei  24192  clssubg  24266  tgphaus  24274  qustgplem  24278  tsmsadd  24304  psmetxrge0  24470  psmetlecl  24472  xmetlecl  24503  xmettpos  24506  imasdsf1olem  24530  imasf1oxmet  24532  imasf1omet  24533  elbl3ps  24548  elbl3  24549  metss  24665  comet  24670  stdbdxmet  24672  stdbdmet  24673  methaus  24677  nrmmetd  24731  abvmet  24732  isngp4  24769  subgngp  24792  nmoi2  24887  nmoleub  24888  nmoid  24899  bl2ioo  24949  zcld  24971  divcn  25027  divccn  25032  cncfcdm  25057  divccncf  25065  icoopnst  25098  clmzlmvsca  25272  cph2ass  25372  tcphcph  25396  cfilfcls  25433  bcthlem2  25484  rrxmet  25567  rrxdstprj1  25568  rrxdsfi  25570  cldcss  25600  dvrec  26114  dvmptfsum  26134  aalioulem3  26497  taylply2  26531  efsubm  26716  dchrelbasd  27403  dchrmulcl  27413  2sqreulem3  27617  pntrmax  27728  padicabv  27794  nosupbnd2  27880  noinfbnd2  27895  sltsd  27961  divmulsw  28386  axtgcont  28738  xmstrkgc  29235  axsegconlem1  29267  axlowdimlem15  29306  usgredg2vlem1  29575  usgredg2vlem2  29576  iswlkon  30005  wwlksnextsurj  30249  elwwlks2  30318  elwspths2spth  30319  frrusgrord  30692  numclwwlk1lem2foalem  30702  grpoidinvlem2  30857  grpoidinvlem3  30858  ablo4  30902  ablomuldiv  30904  nvaddsub4  31009  nvmeq0  31010  sspmval  31085  sspimsval  31090  lnosub  31111  dipsubdir  31200  hvadd4  31388  hvpncan  31391  his35  31440  hiassdi  31443  shscli  31669  shmodsi  31741  chj4  31887  spansnmul  31916  spansncol  31920  spanunsni  31931  hoadd4  32136  hosubadd4  32166  lnopl  32266  unopf1o  32268  counop  32273  lnfnl  32283  hmopadj2  32293  eighmre  32315  lnopmi  32352  lnophsi  32353  hmops  32372  hmopm  32373  cnlnadjlem2  32420  adjmul  32444  adjadd  32445  kbass6  32473  mdslj1i  32671  mdslj2i  32672  mdslmd1lem1  32677  mdslmd2i  32682  chirredlem3  32744  isoun  33047  xdivmul  33244  odutos  33288  lmodvslmhm  33370  isarchi2  33505  archiabllem2  33517  imasmhm  33674  imasghm  33675  imasrhm  33676  imaslmhm  33677  quslmhm  33679  tngdim  34003  fedgmullem2  34020  metider  34284  pl1cn  34345  rossros  34570  ismeas  34589  dya2iocnei  34672  inelcarsg  34701  signstfvc  34961  bnj563  35132  fisshasheq  35606  cnpconn  35722  cvmseu  35768  elmrsubrn  36012  mrsubco  36013  fneint  36879  fnessref  36888  tailfb  36908  onsucuni3  38033  pibt2  38083  ptrecube  38291  poimirlem4  38295  heicant  38326  mblfinlem1  38328  mblfinlem2  38329  mblfinlem3  38330  mblfinlem4  38331  cnambfre  38339  itg2addnclem2  38343  ftc1anclem5  38368  ftc1anclem6  38369  metf1o  38426  isbnd3b  38456  equivbnd  38461  heiborlem3  38484  rrnmet  38500  rrndstprj1  38501  rrntotbnd  38507  exidcl  38547  ghomco  38562  ghomdiv  38563  grpokerinj  38564  rngoneglmul  38614  rngonegrmul  38615  rngosubdi  38616  rngosubdir  38617  isdrngo2  38629  rngohomco  38645  rngoisocnv  38652  riscer  38659  crngm4  38674  crngohomfo  38677  idlsubcl  38694  inidl  38701  keridl  38703  ispridlc  38741  pridlc3  38744  dmncan1  38747  lflvscl  39871  3dim0  40251  linepsubN  40546  cdlemg2fvlem  41388  trlcoat  41517  istendod  41556  dva1dim  41779  dvhvaddcomN  41890  dihf11  42061  dihlatat  42131  sn-sup2  43285  fsuppssind  43345  mhphf  43349  ismrc  43452  isnacs3  43461  mzpindd  43497  pellex  43582  monotoddzzfi  43689  lermxnn0  43697  rmyeq0  43700  rmyeq  43701  lermy  43702  jm2.27  43755  lsmfgcl  43821  fsumcnsrcl  43913  rngunsnply  43916  gsumws3  44942  mnringmulrcld  44972  nzin  45048  ofdivrec  45056  ofdivcan4  45057  chordthmALT  45661  wessf1ornlem  45923  projf1o  45934  ltdiv23neg  46129  fmulcl  46317  prproropf1olem2  48273  prproropf1olem4  48275  mgmplusgiopALT  48979  idomcanl  49132  itsclc0xyqsolb  49570  toslat  49780  cicerALT  49844