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  1182  3adant3r2  1183  3adant3r3  1184  mp3an1  1449  sotri  6129  fnfco  6754  mpoeq3dva  7493  oprres  7584  fovcdmda  7587  fnmpoovd  8095  offval22  8096  bropfvvvvlem  8099  fnsuppres  8199  suppsssn  8209  sprmpod  8232  oaass  8582  omlimcl  8599  odi  8600  nnmsucr  8646  nnasmo  8684  unfi  9194  ttrclse  9750  cflim2  10286  mulcanenq  10983  mul4  11412  add4  11465  2addsub  11505  addsubeq4  11506  subadd4  11536  muladd  11678  ltleadd  11729  divmul  11908  divne0  11917  div23  11924  div12  11927  div11  11933  divsubdir  11944  subdivcomb1  11945  divcan5  11952  divmuleq  11955  divcan6  11957  divdiv32  11958  div2sub  12075  letrp1  12094  lemul12b  12107  lediv1  12116  lt2mul2div  12129  lemuldiv  12131  ltdiv2  12137  ledivdiv  12140  lediv2  12141  ltdiv23  12142  lediv23  12143  sup2  12207  cju  12245  nndivre  12290  nndivtr  12296  nn0addge1  12556  nn0addge2  12557  peano2uz2  12690  uzind  12694  uzind3  12696  fzind  12700  fnn0ind  12701  uzind4  12931  qre  12978  irrmul  12999  rpdivcl  13043  rerpdivcl  13048  xrinfmsslem  13333  ixxin  13387  iccshftr  13509  iccshftl  13511  iccdil  13513  icccntr  13515  fzaddel  13581  fzadd2  13582  fzrev  13610  modlt  13903  modcyc  13929  axdc4uzlem  14007  expdiv  14137  fundmge2nop0  14524  swrd00  14665  swrdcl  14666  swrdnnn0nd  14677  swrd0  14679  swrdwrdsymb  14683  ccatpfx  14722  swrdccat  14756  splid  14774  swrdco  14859  2shfti  15102  isermulc2  15677  fsummulc2  15803  dvdscmulr  16305  dvdsmulcr  16306  dvds2add  16310  dvds2sub  16311  dvdstr  16314  alzdvds  16340  divalg2  16425  dvdslegcd  16524  lcmgcdlem  16626  lcmgcdeq  16632  isprm6  16734  pcqcl  16877  vdwmc2  17000  ressinbas  17272  cicer  17826  isposd  18343  pleval2i  18355  poslubmo  18430  posglbmo  18431  tosso  18438  mgmplusf  18637  ismgmd  18639  grpinva  18661  idmgmhm  18688  resmgmhm  18698  resmgmhm2  18699  resmgmhm2b  18700  mgmhmco  18701  mgmhmima  18702  submgmacs  18704  sgrpidmnd  18726  ismndd  18743  imasmnd2  18761  idmhm  18782  mndvcl  18784  issubm2  18791  0mhm  18806  resmhm  18807  resmhm2  18808  resmhm2b  18809  mhmco  18810  mhmimalem  18811  submacs  18814  prdspjmhm  18816  pwsdiagmhm  18818  pwsco1mhm  18819  pwsco2mhm  18820  gsumwsubmcl  18824  gsumsgrpccat  18827  gsumwmhm  18832  grpinvcnv  18998  grpinvnzcl  19003  grpsubf  19011  imasgrp2  19047  qusgrp2  19050  mhmfmhm  19057  mulgnnsubcl  19078  mulgnndir  19095  issubg4  19137  isnsg3  19152  nsgacs  19154  nsgid  19162  qusadd  19180  qus0subgadd  19191  ghmmhm  19218  ghmmhmb  19219  idghm  19223  resghm  19224  ghmf1  19238  qusghm  19247  gaid  19291  subgga  19292  gasubg  19294  invoppggim  19352  gsmsymgrfix  19419  smndlsmidm  19647  pj1ghm  19694  mulgnn0di  19816  mulgmhm  19818  mulgghm  19819  ghmfghm  19821  invghm  19824  ghmplusg  19837  ablnsg  19838  qusabl  19856  gsumval3eu  19895  gsumval3  19898  gsumzcl2  19901  gsumzaddlem  19912  gsumzadd  19913  gsumzmhm  19928  gsumzoppg  19935  srgfcl  20166  srgcom4lem  20183  srgmulgass  20187  srglmhm  20191  srgrmhm  20192  ringcomlem  20249  ringlghm  20282  ringrghm  20283  pwspjmhmmgpd  20298  c0mgm  20432  c0mhm  20433  isnzr2  20491  subrngringnsg  20526  issubrng2  20531  rhmimasubrnglem  20538  issubrg2  20565  domnmuln0  20682  isdomn3  20688  issrngd  20829  islmodd  20837  lmodscaf  20855  lcomf  20872  lmodvsghm  20894  rmodislmodlem  20900  lssacs  20938  idlmhm  21013  invlmhm  21014  lmhmvsca  21017  reslmhm2  21025  reslmhm2b  21026  pwsdiaglmhm  21029  pwssplit2  21032  pwssplit3  21033  issubrgd  21163  qusrhm  21253  qusmul2idl  21256  crngridl  21257  qusmulrng  21259  expmhm  21421  zntoslem  21542  znfld  21546  psgnghm  21565  phlipf  21637  frlmup1  21785  asclghm  21870  asclrhm  21877  rnasclmulcl  21881  psraddcl  21925  psraddclOLD  21926  psrvscacl  21938  psrass23  21956  psrbagev1  22068  coe1sclmulfv  22253  cply1mul  22267  evls1fpws  22340  rhmply1vsca  22359  matbas2d  22396  submaeval  22555  minmar1eval  22622  cpmatacl  22689  pmatcollpw1  22749  pmatcollpw  22754  tgclb  22943  topbas  22945  ntrss  23028  mretopd  23065  neissex  23100  cnpnei  23237  lmcnp  23277  ordthaus  23357  llynlly  23450  restnlly  23455  llyidm  23461  nllyidm  23462  ptbasin  23550  txcnp  23593  ist0-4  23702  kqt0lem  23709  isr0  23710  regr1lem2  23713  cmphmph  23761  connhmph  23762  fbun  23813  trfbas2  23816  isfil2  23829  isfild  23831  infil  23836  fbasfip  23841  fbasrn  23857  trfil2  23860  rnelfmlem  23925  fmfnfmlem3  23929  flimopn  23948  txflf  23979  fclsnei  23992  fclsfnflim  24000  fcfnei  24008  clssubg  24082  tgphaus  24090  qustgplem  24094  tsmsadd  24120  psmetxrge0  24287  psmetlecl  24289  xmetlecl  24320  xmettpos  24323  imasdsf1olem  24347  imasf1oxmet  24349  imasf1omet  24350  elbl3ps  24365  elbl3  24366  metss  24484  comet  24489  stdbdxmet  24491  stdbdmet  24492  methaus  24496  nrmmetd  24550  abvmet  24551  isngp4  24588  subgngp  24611  nmoi2  24706  nmoleub  24707  nmoid  24718  bl2ioo  24768  zcld  24790  divcnOLD  24845  divcn  24847  divccn  24852  divccnOLD  24854  cncfcdm  24879  divccncf  24887  icoopnst  24924  clmzlmvsca  25101  cph2ass  25202  tcphcph  25226  cfilfcls  25263  bcthlem2  25314  rrxmet  25397  rrxdstprj1  25398  rrxdsfi  25400  cldcss  25430  dvrec  25948  dvmptfsum  25968  aalioulem3  26331  taylply2  26364  taylply2OLD  26365  efsubm  26548  dchrelbasd  27238  dchrmulcl  27248  2sqreulem3  27452  pntrmax  27563  padicabv  27629  nosupbnd2  27716  noinfbnd2  27731  ssltd  27791  divsmulw  28173  axtgcont  28432  xmstrkgc  28850  axsegconlem1  28881  axlowdimlem15  28920  usgredg2vlem1  29189  usgredg2vlem2  29190  iswlkon  29622  wwlksnextsurj  29867  elwwlks2  29933  elwspths2spth  29934  frrusgrord  30307  numclwwlk1lem2foalem  30317  grpoidinvlem2  30471  grpoidinvlem3  30472  ablo4  30516  ablomuldiv  30518  nvaddsub4  30623  nvmeq0  30624  sspmval  30699  sspimsval  30704  lnosub  30725  dipsubdir  30814  hvadd4  31002  hvpncan  31005  his35  31054  hiassdi  31057  shscli  31283  shmodsi  31355  chj4  31501  spansnmul  31530  spansncol  31534  spanunsni  31545  hoadd4  31750  hosubadd4  31780  lnopl  31880  unopf1o  31882  counop  31887  lnfnl  31897  hmopadj2  31907  eighmre  31929  lnopmi  31966  lnophsi  31967  hmops  31986  hmopm  31987  cnlnadjlem2  32034  adjmul  32058  adjadd  32059  kbass6  32087  mdslj1i  32285  mdslj2i  32286  mdslmd1lem1  32291  mdslmd2i  32296  chirredlem3  32358  isoun  32658  xdivmul  32854  odutos  32904  lmodvslmhm  32999  isarchi2  33138  archiabllem2  33150  imasmhm  33323  imasghm  33324  imasrhm  33325  imaslmhm  33326  quslmhm  33328  tngdim  33605  fedgmullem2  33622  metider  33834  pl1cn  33895  rossros  34122  ismeas  34141  dya2iocnei  34225  inelcarsg  34254  signstfvc  34530  bnj563  34698  fisshasheq  35061  cnpconn  35176  cvmseu  35222  elmrsubrn  35466  mrsubco  35467  fneint  36290  fnessref  36299  tailfb  36319  onsucuni3  37309  pibt2  37359  ptrecube  37568  poimirlem4  37572  heicant  37603  mblfinlem1  37605  mblfinlem2  37606  mblfinlem3  37607  mblfinlem4  37608  cnambfre  37616  itg2addnclem2  37620  ftc1anclem5  37645  ftc1anclem6  37646  metf1o  37703  isbnd3b  37733  equivbnd  37738  heiborlem3  37761  rrnmet  37777  rrndstprj1  37778  rrntotbnd  37784  exidcl  37824  ghomco  37839  ghomdiv  37840  grpokerinj  37841  rngoneglmul  37891  rngonegrmul  37892  rngosubdi  37893  rngosubdir  37894  isdrngo2  37906  rngohomco  37922  rngoisocnv  37929  riscer  37936  crngm4  37951  crngohomfo  37954  idlsubcl  37971  inidl  37978  keridl  37980  ispridlc  38018  pridlc3  38021  dmncan1  38024  lflvscl  39019  3dim0  39400  linepsubN  39695  cdlemg2fvlem  40537  trlcoat  40666  istendod  40705  dva1dim  40928  dvhvaddcomN  41039  dihf11  41210  dihlatat  41280  metakunt12  42158  sn-sup2  42446  fsuppssind  42548  mhphf  42552  ismrc  42657  isnacs3  42666  mzpindd  42702  pellex  42791  monotoddzzfi  42899  lermxnn0  42907  rmyeq0  42910  rmyeq  42911  lermy  42912  jm2.27  42965  lsmfgcl  43031  fsumcnsrcl  43123  rngunsnply  43126  gsumws3  44154  mnringmulrcld  44192  nzin  44282  ofdivrec  44290  ofdivcan4  44291  chordthmALT  44898  wessf1ornlem  45135  projf1o  45147  ltdiv23neg  45350  fmulcl  45541  prproropf1olem2  47437  prproropf1olem4  47439  mgmplusgiopALT  48056  itsclc0xyqsolb  48637  toslat  48827