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 424	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3expia  1139  3adant3r1  1201  3adant3r2  1202  3adant3r3  1203  mp3an1  1477  sotri  6121  fnfco  6741  mpoeq3dva  7491  oprres  7582  fovcdmda  7586  fnmpoovd  8085  offval22  8086  bropfvvvvlem  8089  fnsuppres  8190  suppsssn  8200  sprmpod  8223  oaass  8551  omlimcl  8568  odi  8569  nnmsucr  8616  nnasmo  8654  unfi  9168  ttrclse  9709  cflim2  10268  mulcanenq  10972  mul4  11405  add4  11458  2addsub  11498  addsubeq4  11499  subadd4  11529  muladd  11673  ltleadd  11724  divmul  11902  divne0  11911  div23  11918  div12  11921  div11  11927  divsubdir  11935  subdivcomb1  11937  divcan5  11944  divmuleq  11947  divcan6  11949  divdiv32  11950  div2sub  12067  letrp1  12086  lemul12b  12099  lediv1  12107  lt2mul2div  12120  lemuldiv  12122  ltdiv2  12128  ledivdiv  12131  lediv2  12132  ltdiv23  12133  lediv23  12134  sup2  12198  cju  12241  nndivre  12304  nndivtr  12310  nn0addge1  12577  nn0addge2  12578  peano2uz2  12712  uzind  12716  uzind3  12718  fzind  12722  fnn0ind  12723  uzind4  12958  qre  13005  irrmul  13027  rpdivcl  13072  rerpdivcl  13077  xrinfmsslem  13363  ixxin  13418  iccshftr  13542  iccshftl  13544  iccdil  13546  icccntr  13548  fzaddel  13616  fzadd2  13617  fzrev  13645  modlt  13944  modcyc  13970  axdc4uzlem  14050  expdiv  14180  fundmge2nop0  14570  swrd00  14715  swrdcl  14716  swrdnnn0nd  14729  swrd0  14731  swrdwrdsymb  14735  ccatpfx  14773  swrdccat  14807  splid  14825  swrdco  14911  2shfti  15156  isermulc2  15748  fsummulc2  15873  dvdscmulr  16377  dvdsmulcr  16378  dvds2add  16383  dvds2sub  16384  dvdstr  16387  alzdvds  16413  divalg2  16498  dvdslegcd  16597  lcmgcdlem  16699  lcmgcdeq  16705  isprm6  16808  pcqcl  16951  vdwmc2  17074  ressinbas  17340  cicer  17898  isposd  18413  pleval2i  18425  poslubmo  18500  posglbmo  18501  tosso  18508  mgmplusf  18743  mgmn0plusgf  18744  ismgmd  18747  grpinva  18771  imasmgm2  18779  qusmgm  18780  idmgmhm  18806  resmgmhm  18816  resmgmhm2  18817  resmgmhm2b  18818  mgmhmco  18819  mgmhmima  18820  submgmacs  18822  sgrpidmnd  18844  ismndd  18862  imasmnd2  18884  qusmnd  18891  idmhm  18906  mndvcl  18908  issubm2  18915  0mhm  18931  resmhm  18932  resmhm2  18933  resmhm2b  18934  mhmco  18935  mhmimalem  18936  submacs  18939  prdspjmhm  18941  pwsdiagmhm  18943  pwsco1mhm  18944  pwsco2mhm  18945  gsumwsubmcl  18949  gsumsgrpccat  18952  gsumwmhm  18957  grpinvcnv  19133  grpinvnzcl  19137  grpsubf  19145  imasgrp2  19181  qusgrp2  19184  mhmfmhm  19191  mulgnnsubcl  19212  mulgnndir  19229  issubg4  19272  isnsg3  19286  nsgacs  19288  nsgid  19296  qusadd  19319  qus0subgadd  19330  ghmmhm  19356  ghmmhmb  19357  idghm  19361  resghm  19362  ghmf1  19376  qusghm  19385  gaid  19429  subgga  19430  gasubg  19432  invoppggim  19490  gsmsymgrfix  19558  smndlsmidm  19786  pj1ghm  19833  mulgnn0di  19955  mulgmhm  19957  mulgghm  19958  ghmfghm  19960  invghm  19963  ghmplusg  19976  ablnsg  19977  qusabl  19995  gsumval3eu  20034  gsumval3  20037  gsumzcl2  20040  gsumzaddlem  20051  gsumzadd  20052  gsumzmhm  20067  gsumzoppg  20074  srgfcl  20338  srgcom4lem  20355  srgmulgass  20359  srglmhm  20363  srgrmhm  20364  ringcomlem  20423  ringlghm  20457  ringrghm  20458  pwspjmhmmgpd  20471  c0mgm  20603  c0mhm  20604  isnzr2  20681  subrngringnsg  20718  issubrng2  20723  rhmimasubrnglem  20730  issubrg2  20757  domnmuln0  20874  isdomn3  20879  isdrng3lem2  20918  issrngd  21024  islmodd  21053  lmodscaf  21071  lcomf  21088  lmodvsghm  21110  rmodislmodlem  21116  lssacs  21154  idlmhm  21228  invlmhm  21229  lmhmvsca  21232  reslmhm2  21240  reslmhm2b  21241  pwsdiaglmhm  21244  pwssplit2  21247  pwssplit3  21248  issubrgd  21376  qusrhm  21481  qusmul2idl  21484  crngridl  21485  qusmulrng  21488  cmprmidlmcl  21541  expmhm  21652  zntoslem  21772  znfld  21776  psgnghm  21796  phlipf  21868  frlmup1  22014  asclghm  22100  asclrhm  22108  rnasclmulcl  22112  psraddcl  22157  psrvscacl  22169  psrass23  22186  psrbagev1  22296  coe1sclmulfv  22512  cply1mul  22524  evls1fpws  22597  rhmply1vsca  22613  matbas2d  22648  submaeval  22807  minmar1eval  22874  cpmatacl  22944  pmatcollpw1  23004  pmatcollpw  23009  tgclb  23198  topbas  23200  ntrss  23283  mretopd  23320  neissex  23355  cnpnei  23492  lmcnp  23532  ordthaus  23612  llynlly  23706  restnlly  23711  llyidm  23717  nllyidm  23718  ptbasin  23806  txcnp  23849  ist0-4  23958  kqt0lem  23965  isr0  23966  regr1lem2  23969  cmphmph  24017  connhmph  24018  fbun  24069  trfbas2  24072  isfil2  24085  isfild  24087  infil  24092  fbasfip  24097  fbasrn  24113  trfil2  24116  rnelfmlem  24181  fmfnfmlem3  24185  flimopn  24204  txflf  24235  fclsnei  24248  fclsfnflim  24256  fcfnei  24264  clssubg  24338  tgphaus  24346  qustgplem  24350  tsmsadd  24376  psmetxrge0  24542  psmetlecl  24544  xmetlecl  24575  xmettpos  24578  imasdsf1olem  24602  imasf1oxmet  24604  imasf1omet  24605  elbl3ps  24620  elbl3  24621  metss  24737  comet  24742  stdbdxmet  24744  stdbdmet  24745  methaus  24749  nrmmetd  24803  abvmet  24804  isngp4  24841  subgngp  24864  nmoi2  24959  nmoleub  24960  nmoid  24971  bl2ioo  25021  zcld  25043  divcn  25099  divccn  25104  cncfcdm  25129  divccncf  25137  icoopnst  25170  clmzlmvsca  25344  cph2ass  25444  tcphcph  25468  cfilfcls  25505  bcthlem2  25556  rrxmet  25639  rrxdstprj1  25640  rrxdsfi  25642  cldcss  25672  dvrec  26185  dvmptfsum  26205  aalioulem3  26573  taylply2  26607  efsubm  26791  dchrelbasd  27478  dchrmulcl  27488  2sqreulem3  27692  pntrmax  27803  padicabv  27869  nosupbnd2  27955  noinfbnd2  27970  sltsd  28036  divmulsw  28461  axtgcont  28813  xmstrkgc  29345  axsegconlem1  29377  axlowdimlem15  29416  usgredg2vlem1  29688  usgredg2vlem2  29689  iswlkon  30118  wwlksnextsurj  30371  elwwlks2  30440  elwspths2spth  30441  frrusgrord  30824  numclwwlk1lem2foalem  30834  grpoidinvlem2  30989  grpoidinvlem3  30990  ablo4  31034  ablomuldiv  31036  nvaddsub4  31141  nvmeq0  31142  sspmval  31217  sspimsval  31222  lnosub  31243  dipsubdir  31332  hvadd4  31520  hvpncan  31523  his35  31572  hiassdi  31575  shscli  31801  shmodsi  31873  chj4  32019  spansnmul  32048  spansncol  32052  spanunsni  32063  hoadd4  32268  hosubadd4  32298  lnopl  32398  unopf1o  32400  counop  32405  lnfnl  32415  hmopadj2  32425  eighmre  32447  lnopmi  32484  lnophsi  32485  hmops  32504  hmopm  32505  cnlnadjlem2  32552  adjmul  32576  adjadd  32577  kbass6  32605  mdslj1i  32803  mdslj2i  32804  mdslmd1lem1  32809  mdslmd2i  32814  chirredlem3  32876  isoun  33177  xdivmul  33373  odutos  33411  lmodvslmhm  33493  isarchi2  33628  archiabllem2  33640  imasmhm  33797  imasghm  33798  imasrhm  33799  imaslmhm  33800  quslmhm  33802  tngdim  34126  fedgmullem2  34143  metider  34407  pl1cn  34468  rossros  34694  ismeas  34713  dya2iocnei  34796  inelcarsg  34825  signstfvc  35085  bnj563  35256  fisshasheq  35720  cnpconn  35812  cvmseu  35858  elmrsubrn  36102  mrsubco  36103  fneint  36970  fnessref  36979  tailfb  36999  onsucuni3  38124  pibt2  38174  ptrecube  38372  poimirlem4  38376  heicant  38407  mblfinlem1  38409  mblfinlem2  38410  mblfinlem3  38411  mblfinlem4  38412  cnambfre  38420  itg2addnclem2  38424  ftc1anclem5  38449  ftc1anclem6  38450  metf1o  38508  isbnd3b  38538  equivbnd  38543  heiborlem3  38566  rrnmet  38582  rrndstprj1  38583  rrntotbnd  38589  exidcl  38629  ghomco  38644  ghomdiv  38645  grpokerinj  38646  rngoneglmul  38696  rngonegrmul  38697  rngosubdi  38698  rngosubdir  38699  isdrngo2  38711  rngohomco  38727  rngoisocnv  38734  riscer  38741  crngm4  38756  crngohomfo  38759  idlsubcl  38776  inidl  38783  keridl  38785  ispridlc  38823  pridlc3  38826  dmncan1  38829  lflvscl  39953  3dim0  40333  linepsubN  40628  cdlemg2fvlem  41470  trlcoat  41599  istendod  41638  dva1dim  41861  dvhvaddcomN  41972  dihf11  42143  dihlatat  42213  sn-sup2  43382  fsuppssind  43442  mhphf  43446  ismrc  43549  isnacs3  43558  mzpindd  43594  pellex  43679  monotoddzzfi  43786  lermxnn0  43794  rmyeq0  43797  rmyeq  43798  lermy  43799  jm2.27  43852  lsmfgcl  43918  fsumcnsrcl  44010  rngunsnply  44013  gsumws3  45039  mnringmulrcld  45069  nzin  45145  ofdivrec  45153  ofdivcan4  45154  chordthmALT  45758  wessf1ornlem  46020  projf1o  46031  ltdiv23neg  46226  fmulcl  46414  prproropf1olem2  48407  prproropf1olem4  48409  mgmplusgiopALT  49112  idomcanl  49265  itsclc0xyqsolb  49703  toslat  49911  cicerALT  49975