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  1183  3adant3r2  1184  3adant3r3  1185  mp3an1  1450  sotri  6073  fnfco  6688  mpoeq3dva  7423  oprres  7514  fovcdmda  7517  fnmpoovd  8017  offval22  8018  bropfvvvvlem  8021  fnsuppres  8121  suppsssn  8131  sprmpod  8154  oaass  8476  omlimcl  8493  odi  8494  nnmsucr  8540  nnasmo  8578  unfi  9080  ttrclse  9617  cflim2  10154  mulcanenq  10851  mul4  11281  add4  11334  2addsub  11374  addsubeq4  11375  subadd4  11405  muladd  11549  ltleadd  11600  divmul  11779  divne0  11788  div23  11795  div12  11798  div11  11804  divsubdir  11815  subdivcomb1  11816  divcan5  11823  divmuleq  11826  divcan6  11828  divdiv32  11829  div2sub  11946  letrp1  11965  lemul12b  11978  lediv1  11987  lt2mul2div  12000  lemuldiv  12002  ltdiv2  12008  ledivdiv  12011  lediv2  12012  ltdiv23  12013  lediv23  12014  sup2  12078  cju  12121  nndivre  12166  nndivtr  12172  nn0addge1  12427  nn0addge2  12428  peano2uz2  12561  uzind  12565  uzind3  12567  fzind  12571  fnn0ind  12572  uzind4  12804  qre  12851  irrmul  12872  rpdivcl  12917  rerpdivcl  12922  xrinfmsslem  13207  ixxin  13262  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  fzaddel  13458  fzadd2  13459  fzrev  13487  modlt  13784  modcyc  13810  axdc4uzlem  13890  expdiv  14020  fundmge2nop0  14409  swrd00  14552  swrdcl  14553  swrdnnn0nd  14564  swrd0  14566  swrdwrdsymb  14570  ccatpfx  14608  swrdccat  14642  splid  14660  swrdco  14744  2shfti  14987  isermulc2  15565  fsummulc2  15691  dvdscmulr  16195  dvdsmulcr  16196  dvds2add  16201  dvds2sub  16202  dvdstr  16205  alzdvds  16231  divalg2  16316  dvdslegcd  16415  lcmgcdlem  16517  lcmgcdeq  16523  isprm6  16625  pcqcl  16768  vdwmc2  16891  ressinbas  17156  cicer  17713  isposd  18228  pleval2i  18240  poslubmo  18315  posglbmo  18316  tosso  18323  mgmplusf  18558  ismgmd  18560  grpinva  18582  idmgmhm  18609  resmgmhm  18619  resmgmhm2  18620  resmgmhm2b  18621  mgmhmco  18622  mgmhmima  18623  submgmacs  18625  sgrpidmnd  18647  ismndd  18664  imasmnd2  18682  idmhm  18703  mndvcl  18705  issubm2  18712  0mhm  18727  resmhm  18728  resmhm2  18729  resmhm2b  18730  mhmco  18731  mhmimalem  18732  submacs  18735  prdspjmhm  18737  pwsdiagmhm  18739  pwsco1mhm  18740  pwsco2mhm  18741  gsumwsubmcl  18745  gsumsgrpccat  18748  gsumwmhm  18753  grpinvcnv  18919  grpinvnzcl  18924  grpsubf  18932  imasgrp2  18968  qusgrp2  18971  mhmfmhm  18978  mulgnnsubcl  18999  mulgnndir  19016  issubg4  19058  isnsg3  19072  nsgacs  19074  nsgid  19082  qusadd  19100  qus0subgadd  19111  ghmmhm  19138  ghmmhmb  19139  idghm  19143  resghm  19144  ghmf1  19158  qusghm  19167  gaid  19211  subgga  19212  gasubg  19214  invoppggim  19272  gsmsymgrfix  19340  smndlsmidm  19568  pj1ghm  19615  mulgnn0di  19737  mulgmhm  19739  mulgghm  19740  ghmfghm  19742  invghm  19745  ghmplusg  19758  ablnsg  19759  qusabl  19777  gsumval3eu  19816  gsumval3  19819  gsumzcl2  19822  gsumzaddlem  19833  gsumzadd  19834  gsumzmhm  19849  gsumzoppg  19856  srgfcl  20114  srgcom4lem  20131  srgmulgass  20135  srglmhm  20139  srgrmhm  20140  ringcomlem  20197  ringlghm  20230  ringrghm  20231  pwspjmhmmgpd  20246  c0mgm  20377  c0mhm  20378  isnzr2  20433  subrngringnsg  20468  issubrng2  20473  rhmimasubrnglem  20480  issubrg2  20507  domnmuln0  20624  isdomn3  20630  issrngd  20770  islmodd  20799  lmodscaf  20817  lcomf  20834  lmodvsghm  20856  rmodislmodlem  20862  lssacs  20900  idlmhm  20975  invlmhm  20976  lmhmvsca  20979  reslmhm2  20987  reslmhm2b  20988  pwsdiaglmhm  20991  pwssplit2  20994  pwssplit3  20995  issubrgd  21123  qusrhm  21213  qusmul2idl  21216  crngridl  21217  qusmulrng  21219  expmhm  21373  zntoslem  21493  znfld  21497  psgnghm  21517  phlipf  21589  frlmup1  21735  asclghm  21820  asclrhm  21827  rnasclmulcl  21831  psraddcl  21875  psraddclOLD  21876  psrvscacl  21888  psrass23  21906  psrbagev1  22012  coe1sclmulfv  22197  cply1mul  22211  evls1fpws  22284  rhmply1vsca  22303  matbas2d  22338  submaeval  22497  minmar1eval  22564  cpmatacl  22631  pmatcollpw1  22691  pmatcollpw  22696  tgclb  22885  topbas  22887  ntrss  22970  mretopd  23007  neissex  23042  cnpnei  23179  lmcnp  23219  ordthaus  23299  llynlly  23392  restnlly  23397  llyidm  23403  nllyidm  23404  ptbasin  23492  txcnp  23535  ist0-4  23644  kqt0lem  23651  isr0  23652  regr1lem2  23655  cmphmph  23703  connhmph  23704  fbun  23755  trfbas2  23758  isfil2  23771  isfild  23773  infil  23778  fbasfip  23783  fbasrn  23799  trfil2  23802  rnelfmlem  23867  fmfnfmlem3  23871  flimopn  23890  txflf  23921  fclsnei  23934  fclsfnflim  23942  fcfnei  23950  clssubg  24024  tgphaus  24032  qustgplem  24036  tsmsadd  24062  psmetxrge0  24228  psmetlecl  24230  xmetlecl  24261  xmettpos  24264  imasdsf1olem  24288  imasf1oxmet  24290  imasf1omet  24291  elbl3ps  24306  elbl3  24307  metss  24423  comet  24428  stdbdxmet  24430  stdbdmet  24431  methaus  24435  nrmmetd  24489  abvmet  24490  isngp4  24527  subgngp  24550  nmoi2  24645  nmoleub  24646  nmoid  24657  bl2ioo  24707  zcld  24729  divcnOLD  24784  divcn  24786  divccn  24791  divccnOLD  24793  cncfcdm  24818  divccncf  24826  icoopnst  24863  clmzlmvsca  25040  cph2ass  25140  tcphcph  25164  cfilfcls  25201  bcthlem2  25252  rrxmet  25335  rrxdstprj1  25336  rrxdsfi  25338  cldcss  25368  dvrec  25886  dvmptfsum  25906  aalioulem3  26269  taylply2  26302  taylply2OLD  26303  efsubm  26487  dchrelbasd  27177  dchrmulcl  27187  2sqreulem3  27391  pntrmax  27502  padicabv  27568  nosupbnd2  27655  noinfbnd2  27670  ssltd  27731  divsmulw  28132  axtgcont  28447  xmstrkgc  28864  axsegconlem1  28895  axlowdimlem15  28934  usgredg2vlem1  29203  usgredg2vlem2  29204  iswlkon  29634  wwlksnextsurj  29878  elwwlks2  29947  elwspths2spth  29948  frrusgrord  30321  numclwwlk1lem2foalem  30331  grpoidinvlem2  30485  grpoidinvlem3  30486  ablo4  30530  ablomuldiv  30532  nvaddsub4  30637  nvmeq0  30638  sspmval  30713  sspimsval  30718  lnosub  30739  dipsubdir  30828  hvadd4  31016  hvpncan  31019  his35  31068  hiassdi  31071  shscli  31297  shmodsi  31369  chj4  31515  spansnmul  31544  spansncol  31548  spanunsni  31559  hoadd4  31764  hosubadd4  31794  lnopl  31894  unopf1o  31896  counop  31901  lnfnl  31911  hmopadj2  31921  eighmre  31943  lnopmi  31980  lnophsi  31981  hmops  32000  hmopm  32001  cnlnadjlem2  32048  adjmul  32072  adjadd  32073  kbass6  32101  mdslj1i  32299  mdslj2i  32300  mdslmd1lem1  32305  mdslmd2i  32310  chirredlem3  32372  isoun  32683  xdivmul  32905  odutos  32949  lmodvslmhm  33030  isarchi2  33154  archiabllem2  33166  imasmhm  33319  imasghm  33320  imasrhm  33321  imaslmhm  33322  quslmhm  33324  tngdim  33626  fedgmullem2  33643  metider  33907  pl1cn  33968  rossros  34193  ismeas  34212  dya2iocnei  34295  inelcarsg  34324  signstfvc  34587  bnj563  34755  fisshasheq  35159  cnpconn  35274  cvmseu  35320  elmrsubrn  35564  mrsubco  35565  fneint  36392  fnessref  36401  tailfb  36421  onsucuni3  37411  pibt2  37461  ptrecube  37670  poimirlem4  37674  heicant  37705  mblfinlem1  37707  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  cnambfre  37718  itg2addnclem2  37722  ftc1anclem5  37747  ftc1anclem6  37748  metf1o  37805  isbnd3b  37835  equivbnd  37840  heiborlem3  37863  rrnmet  37879  rrndstprj1  37880  rrntotbnd  37886  exidcl  37926  ghomco  37941  ghomdiv  37942  grpokerinj  37943  rngoneglmul  37993  rngonegrmul  37994  rngosubdi  37995  rngosubdir  37996  isdrngo2  38008  rngohomco  38024  rngoisocnv  38031  riscer  38038  crngm4  38053  crngohomfo  38056  idlsubcl  38073  inidl  38080  keridl  38082  ispridlc  38120  pridlc3  38123  dmncan1  38126  lflvscl  39186  3dim0  39566  linepsubN  39861  cdlemg2fvlem  40703  trlcoat  40832  istendod  40871  dva1dim  41094  dvhvaddcomN  41205  dihf11  41376  dihlatat  41446  sn-sup2  42594  fsuppssind  42696  mhphf  42700  ismrc  42804  isnacs3  42813  mzpindd  42849  pellex  42938  monotoddzzfi  43045  lermxnn0  43053  rmyeq0  43056  rmyeq  43057  lermy  43058  jm2.27  43111  lsmfgcl  43177  fsumcnsrcl  43269  rngunsnply  43272  gsumws3  44299  mnringmulrcld  44331  nzin  44421  ofdivrec  44429  ofdivcan4  44430  chordthmALT  45035  wessf1ornlem  45292  projf1o  45304  ltdiv23neg  45502  fmulcl  45691  prproropf1olem2  47614  prproropf1olem4  47616  mgmplusgiopALT  48304  itsclc0xyqsolb  48881  toslat  49092  cicerALT  49157