Theorem 3expb 1116

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

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

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 1085

This theorem is referenced by:  3expia  1117  3adant3r1  1178  3adant3r2  1179  3adant3r3  1180  mp3an1  1444  sotri  5987  fnfco  6543  mpoeq3dva  7231  oprres  7316  fovrnda  7319  fnmpoovd  7782  offval22  7783  bropfvvvvlem  7786  fnsuppres  7857  suppsssn  7865  sprmpod  7890  oaass  8187  omlimcl  8204  odi  8205  nnmsucr  8251  cflim2  9685  mulcanenq  10382  mul4  10808  add4  10860  2addsub  10900  addsubeq4  10901  subadd4  10930  muladd  11072  ltleadd  11123  divmul  11301  divne0  11310  div23  11317  div12  11320  divsubdir  11334  subdivcomb1  11335  divcan5  11342  divmuleq  11345  divcan6  11347  divdiv32  11348  div2sub  11465  letrp1  11484  lemul12b  11497  lediv1  11505  lt2mul2div  11518  lemuldiv  11520  ltdiv2  11526  ledivdiv  11529  lediv2  11530  ltdiv23  11531  lediv23  11532  sup2  11597  cju  11634  nndivre  11679  nndivtr  11685  nn0addge1  11944  nn0addge2  11945  peano2uz2  12071  uzind  12075  uzind3  12077  fzind  12081  fnn0ind  12082  uzind4  12307  qre  12354  irrmul  12374  rpdivcl  12415  rerpdivcl  12420  xrinfmsslem  12702  ixxin  12756  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  fzaddel  12942  fzadd2  12943  fzrev  12971  modlt  13249  modcyc  13275  axdc4uzlem  13352  expdiv  13481  fundmge2nop0  13851  ccat2s1fvwOLD  13999  swrd00  14006  swrdcl  14007  swrdnnn0nd  14018  swrd0  14020  swrdwrdsymb  14024  ccatpfx  14063  swrdccat  14097  splid  14115  swrdco  14199  2shfti  14439  isermulc2  15014  fsummulc2  15139  dvdscmulr  15638  dvdsmulcr  15639  dvds2add  15643  dvds2sub  15644  dvdstr  15646  alzdvds  15670  divalg2  15756  dvdslegcd  15853  lcmgcdlem  15950  lcmgcdeq  15956  isprm6  16058  pcqcl  16193  vdwmc2  16315  ressinbas  16560  cicer  17076  isposd  17565  pleval2i  17574  tosso  17646  poslubmo  17756  posglbmo  17757  mgmplusf  17862  grprinvd  17884  sgrpidmnd  17916  ismndd  17933  imasmnd2  17948  idmhm  17965  issubm2  17969  0mhm  17984  resmhm  17985  resmhm2  17986  resmhm2b  17987  mhmco  17988  mhmima  17989  submacs  17991  prdspjmhm  17993  pwsdiagmhm  17995  pwsco1mhm  17996  pwsco2mhm  17997  gsumwsubmcl  18001  gsumsgrpccat  18004  gsumccatOLD  18005  gsumwmhm  18010  grpinvcnv  18167  grpinvnzcl  18171  grpsubf  18178  imasgrp2  18214  qusgrp2  18217  mhmfmhm  18222  mulgnnsubcl  18240  mulgnndir  18256  issubg4  18298  isnsg3  18312  nsgacs  18314  nsgid  18322  qusadd  18337  ghmmhm  18368  ghmmhmb  18369  idghm  18373  resghm  18374  ghmf1  18387  qusghm  18395  gaid  18429  subgga  18430  gasubg  18432  invoppggim  18488  gsmsymgrfix  18556  smndlsmidm  18781  lsmidmOLD  18789  pj1ghm  18829  mulgnn0di  18946  mulgmhm  18948  mulgghm  18949  ghmfghm  18951  invghm  18954  ghmplusg  18966  ablnsg  18967  qusabl  18985  gsumval3eu  19024  gsumval3  19027  gsumzcl2  19030  gsumzaddlem  19041  gsumzadd  19042  gsumzmhm  19057  gsumzoppg  19064  srgfcl  19265  srgmulgass  19281  srglmhm  19285  srgrmhm  19286  ringlghm  19354  ringrghm  19355  issubrg2  19555  issrngd  19632  islmodd  19640  lmodscaf  19656  lcomf  19673  lmodvsghm  19695  rmodislmodlem  19701  lssacs  19739  idlmhm  19813  invlmhm  19814  lmhmvsca  19817  reslmhm2  19825  reslmhm2b  19826  pwsdiaglmhm  19829  pwssplit2  19832  pwssplit3  19833  issubrngd2  19961  qusrhm  20010  crngridl  20011  quscrng  20013  isnzr2  20036  domnmuln0  20071  opprdomn  20074  asclghm  20112  asclrhm  20119  rnasclmulcl  20123  psraddcl  20163  psrvscacl  20173  psrass23  20190  psrbagev1  20290  coe1sclmulfv  20451  cply1mul  20462  expmhm  20614  zntoslem  20703  znfld  20707  psgnghm  20724  phlipf  20796  frlmup1  20942  mndvcl  21002  matbas2d  21032  submaeval  21191  minmar1eval  21258  cpmatacl  21324  pmatcollpw1  21384  pmatcollpw  21389  tgclb  21578  topbas  21580  ntrss  21663  mretopd  21700  neissex  21735  cnpnei  21872  lmcnp  21912  ordthaus  21992  llynlly  22085  restnlly  22090  llyidm  22096  nllyidm  22097  ptbasin  22185  txcnp  22228  ist0-4  22337  kqt0lem  22344  isr0  22345  regr1lem2  22348  cmphmph  22396  connhmph  22397  fbun  22448  trfbas2  22451  isfil2  22464  isfild  22466  infil  22471  fbasfip  22476  fbasrn  22492  trfil2  22495  rnelfmlem  22560  fmfnfmlem3  22564  flimopn  22583  txflf  22614  fclsnei  22627  fclsfnflim  22635  fcfnei  22643  clssubg  22717  tgphaus  22725  qustgplem  22729  tsmsadd  22755  psmetxrge0  22923  psmetlecl  22925  xmetlecl  22956  xmettpos  22959  imasdsf1olem  22983  imasf1oxmet  22985  imasf1omet  22986  elbl3ps  23001  elbl3  23002  metss  23118  comet  23123  stdbdxmet  23125  stdbdmet  23126  methaus  23130  nrmmetd  23184  abvmet  23185  isngp4  23221  subgngp  23244  nmoi2  23339  nmoleub  23340  nmoid  23351  bl2ioo  23400  zcld  23421  divcn  23476  divccn  23481  cncffvrn  23506  divccncf  23514  icoopnst  23543  clmzlmvsca  23717  cph2ass  23817  tcphcph  23840  cfilfcls  23877  bcthlem2  23928  rrxmet  24011  rrxdstprj1  24012  rrxdsfi  24014  cldcss  24044  dvrec  24552  dvmptfsum  24572  aalioulem3  24923  taylply2  24956  efsubm  25135  dchrelbasd  25815  dchrmulcl  25825  2sqreulem3  26029  pntrmax  26140  padicabv  26206  axtgcont  26255  xmstrkgc  26672  axsegconlem1  26703  axlowdimlem15  26742  usgredg2vlem1  27007  usgredg2vlem2  27008  iswlkon  27439  wwlksnextsurj  27678  elwwlks2  27745  elwspths2spth  27746  frrusgrord  28120  numclwwlk1lem2foalem  28130  grpoidinvlem2  28282  grpoidinvlem3  28283  ablo4  28327  ablomuldiv  28329  nvaddsub4  28434  nvmeq0  28435  sspmval  28510  sspimsval  28515  lnosub  28536  dipsubdir  28625  hvadd4  28813  hvpncan  28816  his35  28865  hiassdi  28868  shscli  29094  shmodsi  29166  chj4  29312  spansnmul  29341  spansncol  29345  spanunsni  29356  hoadd4  29561  hosubadd4  29591  lnopl  29691  unopf1o  29693  counop  29698  lnfnl  29708  hmopadj2  29718  eighmre  29740  lnopmi  29777  lnophsi  29778  hmops  29797  hmopm  29798  cnlnadjlem2  29845  adjmul  29869  adjadd  29870  kbass6  29898  mdslj1i  30096  mdslj2i  30097  mdslmd1lem1  30102  mdslmd2i  30107  chirredlem3  30169  isoun  30437  xdivmul  30601  odutos  30650  lmodvslmhm  30688  isarchi2  30814  archiabllem2  30826  quslmhm  30924  tngdim  31011  fedgmullem2  31026  metider  31134  pl1cn  31198  rossros  31439  ismeas  31458  dya2iocnei  31540  inelcarsg  31569  signstfvc  31844  bnj563  32014  fisshasheq  32352  cnpconn  32477  cvmseu  32523  elmrsubrn  32767  mrsubco  32768  nosupbnd2  33216  fneint  33696  fnessref  33705  tailfb  33725  onsucuni3  34651  pibt2  34701  ptrecube  34907  poimirlem4  34911  heicant  34942  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  cnambfre  34955  itg2addnclem2  34959  ftc1anclem5  34986  ftc1anclem6  34987  metf1o  35045  isbnd3b  35078  equivbnd  35083  heiborlem3  35106  rrnmet  35122  rrndstprj1  35123  rrntotbnd  35129  exidcl  35169  ghomco  35184  ghomdiv  35185  grpokerinj  35186  rngoneglmul  35236  rngonegrmul  35237  rngosubdi  35238  rngosubdir  35239  isdrngo2  35251  rngohomco  35267  rngoisocnv  35274  riscer  35281  crngm4  35296  crngohomfo  35299  idlsubcl  35316  inidl  35323  keridl  35325  ispridlc  35363  pridlc3  35366  dmncan1  35369  lflvscl  36228  3dim0  36608  linepsubN  36903  cdlemg2fvlem  37745  trlcoat  37874  istendod  37913  dva1dim  38136  dvhvaddcomN  38247  dihf11  38418  dihlatat  38488  ismrc  39318  isnacs3  39327  mzpindd  39363  pellex  39452  monotoddzzfi  39559  lermxnn0  39567  rmyeq0  39570  rmyeq  39571  lermy  39572  jm2.27  39625  lsmfgcl  39694  fsumcnsrcl  39786  rngunsnply  39793  isdomn3  39824  gsumws3  40569  nzin  40670  ofdivrec  40678  ofdivcan4  40679  chordthmALT  41287  wessf1ornlem  41465  projf1o  41479  ltdiv23neg  41686  fmulcl  41882  prproropf1olem2  43686  prproropf1olem4  43688  ismgmd  44063  idmgmhm  44075  resmgmhm  44085  resmgmhm2  44086  resmgmhm2b  44087  mgmhmco  44088  mgmhmima  44089  submgmacs  44091  mgmplusgiopALT  44121  c0mgm  44200  c0mhm  44201  itsclc0xyqsolb  44777