Theorem 3expa 1118

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1119 and pm3.2an3 1341 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 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbir 235	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-3an 1088

This theorem is referenced by:  3exp  1119  ad4ant123  1173  ad4ant124  1174  ad4ant134  1175  ad4ant234  1176  ad5ant123  1366  3anidm23  1423  mp3an2  1451  mpd3an3  1464  rgen3  3183  vtocl3  3536  spc3egv  3572  moi2  3690  sbc3ie  3834  2if2  4547  preq12bg  4820  ralxfrd2  5370  reuhypd  5377  otsndisj  5482  funcnvqp  6583  fvtp1g  7175  fntpb  7186  f1imass  7242  weisoeq  7333  f1ofveu  7384  f1ocnvfv3  7385  funeldmdif  8030  curry1f  8088  curry2f  8090  funsssuppss  8172  frrlem13  8280  tfrlem11  8359  oalimcl  8527  oeordsuc  8561  oelim2  8562  nneob  8623  nadd4  8665  mapxpen  9113  findcard  9133  enfii  9156  domtrfil  9162  domnsymfi  9170  phplem2  9175  php  9177  wemaplem3  9508  en2eqpr  9967  infxpabs  10171  infxp  10174  cfflb  10219  cfsmolem  10230  isf32lem12  10324  fin1a2lem9  10368  fin1a2s  10374  axcc3  10398  axdc3lem4  10413  zornn0g  10465  pwfseqlem4  10622  tskwun  10744  tskint  10745  tskxp  10747  tskmap  10748  gruf  10771  grutsk1  10781  addcanpi  10859  ltapi  10863  mul4  11349  add4  11402  2addsub  11442  addsubeq4  11443  muladd  11617  ltleadd  11668  receu  11830  p1le  12034  mulgt1  12051  lbinf  12143  zdiv  12611  fzind  12639  fnn0ind  12640  fzindd  12643  uzss  12823  zbtwnre  12912  qmulcl  12933  qreccl  12935  xrlttr  13107  xaddass  13216  xmulasslem3  13253  xadddilem  13261  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  ioo0  13338  ico0  13359  ioc0  13360  icc0  13361  iooshf  13394  prunioo  13449  ioojoin  13451  elfz5  13484  elfz0fzfz0  13601  elfzonelfzo  13737  fzind2  13753  modaddb  13878  mulexpz  14074  expsub  14082  digit1  14209  facndiv  14260  faclbnd4lem4  14268  faclbnd4  14269  faclbnd5  14270  bccmpl  14281  bcval5  14290  bcpasc  14293  hashunx  14358  hashunsnggt  14366  hashdmpropge2  14455  ccatrn  14561  swrdspsleq  14637  swrdccat2  14641  ccatpfx  14673  pfxccat1  14674  swrdswrd  14677  cshf1  14782  crim  15088  absmax  15303  ello12r  15490  elo12r  15501  climshftlem  15547  2sumeq2dv  15678  hash2iun  15796  expcnv  15837  2cprodeq2dv  15898  rpnnen2lem7  16195  dvdsval3  16233  dvdsnegb  16250  muldvds1  16257  muldvds2  16258  dvdscmul  16259  dvdsmulc  16260  dvdsmulcr  16262  dvds2ln  16266  divalgb  16381  ndvdssub  16386  gcddiv  16528  lcmfval  16598  lcmfcl  16605  dvdslcmf  16608  rpexp1i  16700  phiprmpw  16753  hashgcdeq  16767  pythagtriplem1  16794  pockthg  16884  infpnlem1  16888  4sqlem3  16928  0ramcl  17001  firest  17402  imasaddfnlem  17498  imasleval  17511  mrerintcl  17565  iscatd  17641  fullestrcsetc  18119  fullsetcestrc  18134  clatleglb  18484  mreclatBAD  18529  pslem  18538  mndind  18762  grplmulf1o  18952  grplactcnv  18982  mulgnn0subcl  19026  mulgsubcl  19027  mulgdir  19045  issubg2  19080  issubgrpd2  19081  nmzsubg  19104  eqgen  19120  cycsubm  19141  cycsubgcl  19145  cycsubgss  19146  ghmmulg  19167  ghmf1  19185  kerf1ghm  19186  conjghm  19188  symgpssefmnd  19333  gsmsymgreqlem2  19368  symgfixfo  19376  odeq  19487  odval2  19488  odf1  19499  dfod2  19501  gexdvds  19521  gexdvds2  19522  gexcl2  19526  gexdvds3  19527  sylow2blem2  19558  efgsp1  19674  efgrelexlemb  19687  cmnbascntr  19742  mulgmhm  19764  mulgghm  19765  iscyggen2  19818  iscyg3  19823  ablsimpgfindlem1  20046  srglmhm  20137  srgrmhm  20138  ringlghm  20228  ringrghm  20229  gsumdixp  20235  dvdsrcl2  20282  crngunit  20294  cntzsubrng  20483  subrgugrp  20507  cntzsubr  20522  rnghmsubcsetclem2  20548  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  sdrgacs  20717  lmodvsdir  20799  lmodvsass  20800  lmodvsghm  20836  lsssubg  20870  lss1d  20876  islbs2  21071  lidlsubg  21140  lidlsubcl  21141  rngqiprngimfo  21218  lpigen  21252  xrsdsreval  21335  expghm  21392  mulgghm2  21393  ip0r  21553  obs2ss  21645  islindf3  21742  scmatscm  22407  scmataddcl  22410  scmatsubcl  22411  scmatfo  22424  matunit  22572  cpmatelimp  22606  cpmatelimp2  22608  cpmatinvcl  22611  cpmatmcl  22613  mat2pmatf  22622  m2cpmf  22636  cpm2mf  22646  m2cpmfo  22650  m2cpminv  22654  decpmataa0  22662  pm2mpf  22692  pm2mpf1  22693  idpm2idmp  22695  pm2mpfo  22708  elcls2  22968  opnnei  23014  innei  23019  iscnp4  23157  cnpnei  23158  iscncl  23163  cnnei  23176  cnconst  23178  ordthauslem  23277  bwth  23304  1stccnp  23356  llyrest  23379  nllyrest  23380  kgenss  23437  xkoccn  23513  kqsat  23625  kqt0lem  23630  isr0  23631  fbssfi  23731  isfild  23752  filconn  23777  trfilss  23783  fgtr  23784  ufileu  23813  ufilen  23824  fmfnfmlem4  23851  fmfnfm  23852  hausflimi  23874  cnpflf2  23894  cnpflf  23895  cnpfcf  23935  cnextcn  23961  tsmsxplem1  24047  tsmsxp  24049  ustuqtop0  24135  ismeti  24220  isxmet2d  24222  elbl2ps  24284  elbl2  24285  xblpnfps  24290  xblpnf  24291  xbln0  24309  blin  24316  blssexps  24321  blssex  24322  blcls  24401  blsscls  24402  metrest  24419  metustbl  24461  psmetutop  24462  nmf2  24488  ngpi  24523  tngngp3  24551  nmdvr  24565  nmoi  24623  nmoix  24624  nmoleub  24626  nghmcn  24640  iccntr  24717  metdsle  24748  icoopnst  24843  iocopnst  24844  icccvx  24855  pi1xfr  24962  isclmi0  25005  iscvsi  25036  cphipval  25150  lmmbr  25165  lmmbr2  25166  iscfil3  25180  iscau2  25184  cfilres  25203  bcthlem1  25231  bcthlem4  25234  bcthlem5  25235  rrxmet  25315  ioombl  25473  iccvolcl  25475  ioovolcl  25478  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  ig1pcl  26091  ig1prsp  26093  aannenlem1  26243  taylplem1  26277  dvtaylp  26285  relogeftb  26500  logdivlt  26537  cxpexp  26584  rpcxpcl  26592  isppw2  27032  vmappw  27033  lgslem4  27218  lgscllem  27222  lgsneg1  27240  lgsne0  27253  nosepdm  27603  ssltdisj  27740  mulscutlem  28041  sltonold  28169  brbtwn2  28839  ax5seglem1  28862  ax5seglem2  28863  axcontlem4  28901  ewlkprop  29538  uspgr2wlkeq  29581  uhgrwkspthlem2  29691  clwlkclwwlkfo  29945  eupth2lem3lem7  30170  frgr3vlem2  30210  3cyclfrgrrn1  30221  4cycl2vnunb  30226  frgrncvvdeqlem8  30242  grpoidinvlem3  30442  isvciOLD  30516  nmcvcn  30631  ipval2lem2  30640  sspimsval  30674  isblo2  30719  nmoo0  30727  blocni  30741  isph  30758  hvadd4  30972  hiassdi  31027  ocsh  31219  chj4  31471  spansncol  31504  pjjsi  31636  hoscl  31681  hodcl  31683  hoadd4  31720  homco1  31737  homulass  31738  hoadddi  31739  hoadddir  31740  unoplin  31856  adjvalval  31873  hmoplin  31878  bralnfn  31884  brafnmul  31887  lnopmi  31936  lnopcoi  31939  hmops  31956  hmopm  31957  nmophmi  31967  lnfncnbd  31993  cnlnadjlem2  32004  adjlnop  32022  adjmul  32028  adjadd  32029  branmfn  32041  kbass5  32056  kbass6  32057  leop2  32060  leopadd  32068  leopmuli  32069  pjimai  32112  atcvatlem  32321  chirredlem2  32327  mdsymlem3  32341  mdsymlem5  32343  sumdmdii  32351  sumdmdlem  32354  cdj3lem2a  32372  cdj3lem2b  32373  cdj3lem3a  32375  cdj3i  32377  nn0difffzod  32736  xreceu  32849  cshwrnid  32890  toslublem  32905  tosglblem  32907  lmodvslmhm  32997  ogrpaddltbi  33039  archiabllem1b  33153  archiabllem2c  33156  archiabl  33159  slmdvsdir  33176  slmdvsass  33177  grplsm0l  33381  pidlnzb  33400  rprmndvdsru  33507  zarcls1  33866  pstmxmet  33894  ordtconnlem1  33921  hasheuni  34082  omsf  34294  ballotlemirc  34530  signswmnd  34555  bnj1204  35009  fineqvac  35094  fisshasheq  35109  revpfxsfxrev  35110  txpconn  35226  cvmscld  35267  satfbrsuc  35360  satfrnmapom  35364  satfun  35405  elmpps  35567  dfrdg2  35790  wsuclem  35820  segconeu  36006  linecom  36145  linethru  36148  lineintmo  36152  fnemeet2  36362  fnejoin2  36364  fvineqsneq  37407  lindsadd  37614  lindsdom  37615  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  heicant  37656  mblfinlem1  37658  mblfinlem3  37660  ismblfin  37662  cnambfre  37669  itg2addnclem2  37673  ftc1anclem1  37694  ftc1anclem5  37698  ftc1anclem6  37699  ftc2nc  37703  areacirclem2  37710  areacirclem4  37712  areacirclem5  37713  areacirc  37714  fzmul  37742  subspopn  37753  isbndx  37783  isbnd2  37784  isbnd3  37785  ssbnd  37789  prdstotbnd  37795  heibor1  37811  rrnmet  37830  rngonegmn1l  37942  rngohomco  37975  rngoisocnv  37982  rngoisoco  37983  crngohomfo  38007  isidlc  38016  rngoidl  38025  prnc  38068  ispridlc  38071  cvrval2  39274  glbconxN  39379  hlrelat5N  39402  cvratlem  39422  cvrat2  39430  athgt  39457  3dim2  39469  llnn0  39517  lplnn0N  39548  lvoln0N  39592  snatpsubN  39751  paddasslem18  39838  pmod1i  39849  lhpexle2  40011  lhpexle3lem  40012  lhpexle3  40013  ldilcnv  40116  trlcnv  40166  trlnidatb  40178  cdleme32snaw  40436  cdleme32fvaw  40440  cdleme42ke  40486  cdlemeg46gf  40534  cdleme50trn12  40553  cdlemg1cex  40589  cdlemb3  40607  tgrpgrplem  40750  tgrpabl  40752  tendoplcl2  40779  tendo0pl  40792  tendoicl  40797  tendoipl  40798  cdlemkid3N  40934  tendoex  40976  erngdvlem4  40992  erngdvlem4-rN  41000  dib1dim  41166  dib1dim2  41169  dihglbcpreN  41301  dihmeetALTN  41328  dih1dimatlem  41330  dihatlat  41335  lcmineqlem1  42024  lcmineqlem3  42026  aks4d1p1  42071  aks4d1p7d1  42077  aks4d1p8  42082  sticksstones1  42141  sticksstones2  42142  sticksstones3  42143  sticksstones8  42148  sticksstones10  42150  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones17  42158  sticksstones19  42160  oddcomabszz  42940  acongtr  42974  rpnnen3lem  43027  islssfg  43066  lmhmfgsplit  43082  unxpwdom3  43091  hbtlem7  43121  iocmbl  43209  ss2iundf  43655  ismnu  44257  grumnudlem  44281  ismnushort  44297  nzss  44313  dvconstbi  44330  bccbc  44341  uzmptshftfval  44342  iccdifprioo  45521  climisp  45751  limsupresxr  45771  liminfresxr  45772  dvnmul  45948  volico  45988  volioore  45995  fourierdlem74  46185  fourierdlem75  46186  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0xp  46434  hspmbllem2  46632  smflimlem3  46778  smfsupmpt  46820  smfinflem  46822  smfinfmpt  46824  smflimsupmpt  46834  smfliminfmpt  46837  funressnbrafv2  47249  uniimaelsetpreimafv  47401  imasetpreimafvbijlemfv1  47408  imasetpreimafvbijlemfo  47410  sprsymrelfo  47502  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  grtrissvtx  47947  gricgrlic  48014  nn0mnd  48171  lcoss  48429  snlindsntorlem  48463  mreclat  48989  aacllem  49794