Theorem 3expa 1118

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1119 and pm3.2an3 1340 by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expa	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		df-3an 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbir 235	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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-3an 1089

This theorem is referenced by:  3exp  1119  ad4ant123  1172  ad4ant124  1173  ad4ant134  1174  ad4ant234  1175  ad5ant123  1364  3anidm23  1421  mp3an2  1449  mpd3an3  1462  rgen3  3210  vtocl3  3579  spc3egv  3616  moi2  3738  sbc3ie  3890  2if2  4603  preq12bg  4878  ralxfrd2  5430  reuhypd  5437  otsndisj  5538  funcnvqp  6642  fvtp1g  7235  fntpb  7246  f1imass  7301  weisoeq  7391  f1ofveu  7442  f1ocnvfv3  7443  funeldmdif  8089  curry1f  8147  curry2f  8149  funsssuppss  8231  frrlem13  8339  tfrlem11  8444  oalimcl  8616  oeordsuc  8650  oelim2  8651  nneob  8712  nadd4  8754  mapxpen  9209  findcard  9229  enfii  9252  domtrfil  9258  domnsymfi  9266  phplem2  9271  php  9273  wemaplem3  9617  en2eqpr  10076  infxpabs  10280  infxp  10283  cfflb  10328  cfsmolem  10339  isf32lem12  10433  fin1a2lem9  10477  fin1a2s  10483  axcc3  10507  axdc3lem4  10522  zornn0g  10574  pwfseqlem4  10731  tskwun  10853  tskint  10854  tskxp  10856  tskmap  10857  gruf  10880  grutsk1  10890  addcanpi  10968  ltapi  10972  mul4  11458  add4  11510  2addsub  11550  addsubeq4  11551  muladd  11722  ltleadd  11773  receu  11935  p1le  12139  mulgt1  12156  lbinf  12248  zdiv  12713  fzind  12741  fnn0ind  12742  fzindd  12745  uzss  12926  zbtwnre  13011  qmulcl  13032  qreccl  13034  xrlttr  13202  xaddass  13311  xmulasslem3  13348  xadddilem  13356  xrsupsslem  13369  xrinfmsslem  13370  supxrunb1  13381  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  iooshf  13486  prunioo  13541  ioojoin  13543  elfz5  13576  elfz0fzfz0  13690  elfzonelfzo  13819  fzind2  13835  mulexpz  14153  expsub  14161  digit1  14286  facndiv  14337  faclbnd4lem4  14345  faclbnd4  14346  faclbnd5  14347  bccmpl  14358  bcval5  14367  bcpasc  14370  hashunx  14435  hashunsnggt  14443  hashdmpropge2  14532  ccatrn  14637  swrdspsleq  14713  swrdccat2  14717  ccatpfx  14749  pfxccat1  14750  swrdswrd  14753  cshf1  14858  crim  15164  absmax  15378  ello12r  15563  elo12r  15574  climshftlem  15620  2sumeq2dv  15753  hash2iun  15871  expcnv  15912  2cprodeq2dv  15973  rpnnen2lem7  16268  dvdsval3  16306  dvdsnegb  16322  muldvds1  16329  muldvds2  16330  dvdscmul  16331  dvdsmulc  16332  dvdsmulcr  16334  dvds2ln  16337  divalgb  16452  ndvdssub  16457  gcddiv  16598  lcmfval  16668  lcmfcl  16675  dvdslcmf  16678  rpexp1i  16770  phiprmpw  16823  hashgcdeq  16836  pythagtriplem1  16863  pockthg  16953  infpnlem1  16957  4sqlem3  16997  0ramcl  17070  firest  17492  imasaddfnlem  17588  imasleval  17601  mrerintcl  17655  iscatd  17731  fullestrcsetc  18220  fullsetcestrc  18235  clatleglb  18588  mreclatBAD  18633  pslem  18642  mndind  18863  grplmulf1o  19053  grplactcnv  19083  mulgnn0subcl  19127  mulgsubcl  19128  mulgdir  19146  issubg2  19181  issubgrpd2  19182  nmzsubg  19205  eqgen  19221  cycsubm  19242  cycsubgcl  19246  cycsubgss  19247  ghmmulg  19268  ghmf1  19286  kerf1ghm  19287  conjghm  19289  symgpssefmnd  19437  gsmsymgreqlem2  19473  symgfixfo  19481  odeq  19592  odval2  19593  odf1  19604  dfod2  19606  gexdvds  19626  gexdvds2  19627  gexcl2  19631  gexdvds3  19632  sylow2blem2  19663  efgsp1  19779  efgrelexlemb  19792  cmnbascntr  19847  mulgmhm  19869  mulgghm  19870  iscyggen2  19923  iscyg3  19928  ablsimpgfindlem1  20151  srglmhm  20248  srgrmhm  20249  ringlghm  20335  ringrghm  20336  gsumdixp  20342  dvdsrcl2  20392  crngunit  20404  cntzsubrng  20593  subrgugrp  20619  cntzsubr  20634  rnghmsubcsetclem2  20654  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  sdrgacs  20824  lmodvsdir  20906  lmodvsass  20907  lmodvsghm  20943  lsssubg  20978  lss1d  20984  islbs2  21179  lidlsubg  21256  lidlsubcl  21257  rngqiprngimfo  21334  lpigen  21368  xrsdsreval  21452  expghm  21509  mulgghm2  21510  ip0r  21678  obs2ss  21772  islindf3  21869  scmatscm  22540  scmataddcl  22543  scmatsubcl  22544  scmatfo  22557  matunit  22705  cpmatelimp  22739  cpmatelimp2  22741  cpmatinvcl  22744  cpmatmcl  22746  mat2pmatf  22755  m2cpmf  22769  cpm2mf  22779  m2cpmfo  22783  m2cpminv  22787  decpmataa0  22795  pm2mpf  22825  pm2mpf1  22826  idpm2idmp  22828  pm2mpfo  22841  elcls2  23103  opnnei  23149  innei  23154  iscnp4  23292  cnpnei  23293  iscncl  23298  cnnei  23311  cnconst  23313  ordthauslem  23412  bwth  23439  1stccnp  23491  llyrest  23514  nllyrest  23515  kgenss  23572  xkoccn  23648  kqsat  23760  kqt0lem  23765  isr0  23766  fbssfi  23866  isfild  23887  filconn  23912  trfilss  23918  fgtr  23919  ufileu  23948  ufilen  23959  fmfnfmlem4  23986  fmfnfm  23987  hausflimi  24009  cnpflf2  24029  cnpflf  24030  cnpfcf  24070  cnextcn  24096  tsmsxplem1  24182  tsmsxp  24184  ustuqtop0  24270  ismeti  24356  isxmet2d  24358  elbl2ps  24420  elbl2  24421  xblpnfps  24426  xblpnf  24427  xbln0  24445  blin  24452  blssexps  24457  blssex  24458  blcls  24540  blsscls  24541  metrest  24558  metustbl  24600  psmetutop  24601  nmf2  24627  ngpi  24662  tngngp3  24698  nmdvr  24712  nmoi  24770  nmoix  24771  nmoleub  24773  nghmcn  24787  iccntr  24862  metdsle  24893  icoopnst  24988  iocopnst  24989  icccvx  25000  pi1xfr  25107  isclmi0  25150  iscvsi  25181  cphipval  25296  lmmbr  25311  lmmbr2  25312  iscfil3  25326  iscau2  25330  cfilres  25349  bcthlem1  25377  bcthlem4  25380  bcthlem5  25381  rrxmet  25461  ioombl  25619  iccvolcl  25621  ioovolcl  25624  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  ig1pcl  26238  ig1prsp  26240  aannenlem1  26388  taylplem1  26422  dvtaylp  26430  relogeftb  26644  logdivlt  26681  cxpexp  26728  rpcxpcl  26736  isppw2  27176  vmappw  27177  lgslem4  27362  lgscllem  27366  lgsneg1  27384  lgsne0  27397  nosepdm  27747  ssltdisj  27884  mulscutlem  28175  sltonold  28301  brbtwn2  28938  ax5seglem1  28961  ax5seglem2  28962  axcontlem4  29000  ewlkprop  29639  uspgr2wlkeq  29682  uhgrwkspthlem2  29790  clwlkclwwlkfo  30041  eupth2lem3lem7  30266  frgr3vlem2  30306  3cyclfrgrrn1  30317  4cycl2vnunb  30322  frgrncvvdeqlem8  30338  grpoidinvlem3  30538  isvciOLD  30612  nmcvcn  30727  ipval2lem2  30736  sspimsval  30770  isblo2  30815  nmoo0  30823  blocni  30837  isph  30854  hvadd4  31068  hiassdi  31123  ocsh  31315  chj4  31567  spansncol  31600  pjjsi  31732  hoscl  31777  hodcl  31779  hoadd4  31816  homco1  31833  homulass  31834  hoadddi  31835  hoadddir  31836  unoplin  31952  adjvalval  31969  hmoplin  31974  bralnfn  31980  brafnmul  31983  lnopmi  32032  lnopcoi  32035  hmops  32052  hmopm  32053  nmophmi  32063  lnfncnbd  32089  cnlnadjlem2  32100  adjlnop  32118  adjmul  32124  adjadd  32125  branmfn  32137  kbass5  32152  kbass6  32153  leop2  32156  leopadd  32164  leopmuli  32165  pjimai  32208  atcvatlem  32417  chirredlem2  32423  mdsymlem3  32437  mdsymlem5  32439  sumdmdii  32447  sumdmdlem  32450  cdj3lem2a  32468  cdj3lem2b  32469  cdj3lem3a  32471  cdj3i  32473  nn0difffzod  32811  xreceu  32886  cshwrnid  32928  toslublem  32945  tosglblem  32947  lmodvslmhm  33033  ogrpaddltbi  33068  archiabllem1b  33172  archiabllem2c  33175  archiabl  33178  slmdvsdir  33195  slmdvsass  33196  grplsm0l  33396  pidlnzb  33415  rprmndvdsru  33522  zarcls1  33815  pstmxmet  33843  ordtconnlem1  33870  hasheuni  34049  omsf  34261  ballotlemirc  34496  signswmnd  34534  bnj1204  34988  fineqvac  35073  fisshasheq  35082  revpfxsfxrev  35083  txpconn  35200  cvmscld  35241  satfbrsuc  35334  satfrnmapom  35338  satfun  35379  elmpps  35541  dfrdg2  35759  wsuclem  35789  segconeu  35975  linecom  36114  linethru  36117  lineintmo  36121  fnemeet2  36333  fnejoin2  36335  fvineqsneq  37378  lindsadd  37573  lindsdom  37574  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  heicant  37615  mblfinlem1  37617  mblfinlem3  37619  ismblfin  37621  cnambfre  37628  itg2addnclem2  37632  ftc1anclem1  37653  ftc1anclem5  37657  ftc1anclem6  37658  ftc2nc  37662  areacirclem2  37669  areacirclem4  37671  areacirclem5  37672  areacirc  37673  fzmul  37701  subspopn  37712  isbndx  37742  isbnd2  37743  isbnd3  37744  ssbnd  37748  prdstotbnd  37754  heibor1  37770  rrnmet  37789  rngonegmn1l  37901  rngohomco  37934  rngoisocnv  37941  rngoisoco  37942  crngohomfo  37966  isidlc  37975  rngoidl  37984  prnc  38027  ispridlc  38030  cvrval2  39230  glbconxN  39335  hlrelat5N  39358  cvratlem  39378  cvrat2  39386  athgt  39413  3dim2  39425  llnn0  39473  lplnn0N  39504  lvoln0N  39548  snatpsubN  39707  paddasslem18  39794  pmod1i  39805  lhpexle2  39967  lhpexle3lem  39968  lhpexle3  39969  ldilcnv  40072  trlcnv  40122  trlnidatb  40134  cdleme32snaw  40392  cdleme32fvaw  40396  cdleme42ke  40442  cdlemeg46gf  40490  cdleme50trn12  40509  cdlemg1cex  40545  cdlemb3  40563  tgrpgrplem  40706  tgrpabl  40708  tendoplcl2  40735  tendo0pl  40748  tendoicl  40753  tendoipl  40754  cdlemkid3N  40890  tendoex  40932  erngdvlem4  40948  erngdvlem4-rN  40956  dib1dim  41122  dib1dim2  41125  dihglbcpreN  41257  dihmeetALTN  41284  dih1dimatlem  41286  dihatlat  41291  lcmineqlem1  41986  lcmineqlem3  41988  aks4d1p1  42033  aks4d1p7d1  42039  aks4d1p8  42044  sticksstones1  42103  sticksstones2  42104  sticksstones3  42105  sticksstones8  42110  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones17  42120  sticksstones19  42122  metakunt29  42190  metakunt30  42191  metakunt31  42192  factwoffsmonot  42199  oddcomabszz  42901  acongtr  42935  rpnnen3lem  42988  islssfg  43027  lmhmfgsplit  43043  unxpwdom3  43052  hbtlem7  43082  iocmbl  43174  ss2iundf  43621  ismnu  44230  grumnudlem  44254  ismnushort  44270  nzss  44286  dvconstbi  44303  bccbc  44314  uzmptshftfval  44315  iccdifprioo  45434  climisp  45667  limsupresxr  45687  liminfresxr  45688  dvnmul  45864  volico  45904  volioore  45911  fourierdlem74  46101  fourierdlem75  46102  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0xp  46350  hspmbllem2  46548  smflimlem3  46694  smfsupmpt  46736  smfinflem  46738  smfinfmpt  46740  smflimsupmpt  46750  smfliminfmpt  46753  funressnbrafv2  47159  uniimaelsetpreimafv  47270  imasetpreimafvbijlemfv1  47277  imasetpreimafvbijlemfo  47279  sprsymrelfo  47371  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  uspgrimprop  47757  grtrissvtx  47795  gricgrlic  47835  nn0mnd  47902  lcoss  48165  snlindsntorlem  48199  mreclat  48669  aacllem  48895