Theorem 3expa 1134

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-3an 1103

This theorem is referenced by:  3exp  1135  ad4ant123  1189  ad4ant124  1190  ad4ant134  1191  ad4ant234  1192  ad5ant123  1385  ad5ant124  1386  ad5ant125  1388  3anidm23  1446  mp3an2  1475  mpd3an3  1488  rgen3  3216  vtocl3  3541  spc3egv  3571  moi2  3688  sbc3ie  3830  2if2  4548  preq12bg  4822  ralxfrd2  5384  reuhypd  5391  otsndisj  5503  funcnvqp  6601  fvtp1g  7197  fntpb  7208  f1imass  7263  weisoeq  7354  f1ofveu  7405  f1ocnvfv3  7406  funeldmdif  8045  curry1f  8101  curry2f  8103  funsssuppss  8186  frrlem13  8295  tfrlem11  8375  oalimcl  8545  oeordsuc  8580  oelim2  8581  nneob  8642  nadd4  8685  mapxpen  9131  findcard  9148  enfii  9170  domtrfil  9176  domnsymfi  9184  phplem2  9189  php  9191  wemaplem3  9510  en2eqpr  9991  infxpabs  10194  infxp  10197  cfflb  10243  cfsmolem  10254  isf32lem12  10348  fin1a2lem9  10392  fin1a2s  10398  axcc3  10422  axdc3lem4  10437  zornn0g  10489  pwfseqlem4  10647  tskwun  10769  tskint  10770  tskxp  10772  tskmap  10773  gruf  10796  grutsk1  10806  addcanpi  10884  ltapi  10888  mul4  11378  add4  11431  2addsub  11471  addsubeq4  11472  muladd  11646  ltleadd  11697  receu  11859  p1le  12060  mulgt1  12076  lbinf  12168  zdiv  12666  fzind  12694  fnn0ind  12695  fzindd  12698  uzss  12885  zbtwnre  12970  qmulcl  12991  qreccl  12993  xrlttr  13165  xaddass  13275  xmulasslem3  13312  xadddilem  13320  xrsupsslem  13333  xrinfmsslem  13334  supxrunb1  13345  ioo0  13397  ico0  13418  ioc0  13419  icc0  13420  iooshf  13453  prunioo  13508  ioojoin  13510  elfz5  13544  elfz0fzfz0  13661  elfzonelfzo  13798  fzind2  13817  modaddb  13942  mulexpz  14138  expsub  14146  digit1  14273  facndiv  14324  faclbnd4lem4  14332  faclbnd4  14333  faclbnd5  14334  bccmpl  14345  bcval5  14354  bcpasc  14357  hashunx  14422  hashunsnggt  14430  hashdmpropge2  14520  ccatrn  14627  swrdspsleq  14703  swrdccat2  14707  ccatpfx  14738  pfxccat1  14739  swrdswrd  14742  cshf1  14847  crim  15166  absmax  15381  ello12r  15568  elo12r  15579  climshftlem  15625  2sumeq2dv  15756  hash2iun  15875  expcnv  15918  2cprodeq2dv  15979  rpnnen2lem7  16276  dvdsval3  16314  dvdsnegb  16331  muldvds1  16338  muldvds2  16339  dvdscmul  16340  dvdsmulc  16341  dvdsmulcr  16343  dvds2ln  16347  divalgb  16462  ndvdssub  16467  gcddiv  16609  lcmfval  16679  lcmfcl  16686  dvdslcmf  16689  rpexp1i  16782  phiprmpw  16835  hashgcdeq  16849  pythagtriplem1  16876  pockthg  16966  infpnlem1  16970  4sqlem3  17010  0ramcl  17083  firest  17485  imasaddfnlem  17582  imasleval  17595  mrerintcl  17649  iscatd  17729  fullestrcsetc  18207  fullsetcestrc  18222  clatleglb  18574  mreclatBAD  18619  pslem  18628  mndind  18887  grplmulf1o  19079  grplactcnv  19109  mulgnn0subcl  19153  mulgsubcl  19154  mulgdir  19172  issubg2  19208  issubgrpd2  19209  nmzsubg  19231  eqgen  19249  cycsubm  19273  cycsubgcl  19277  cycsubgss  19278  ghmmulg  19298  ghmf1  19316  kerf1ghm  19317  conjghm  19319  symgpssefmnd  19466  gsmsymgreqlem2  19501  symgfixfo  19509  odeq  19620  odval2  19621  odf1  19632  dfod2  19634  gexdvds  19654  gexdvds2  19655  gexcl2  19659  gexdvds3  19660  sylow2blem2  19691  efgsp1  19807  efgrelexlemb  19820  cmnbascntr  19875  mulgmhm  19897  mulgghm  19898  iscyggen2  19951  iscyg3  19956  ablsimpgfindlem1  20179  ogrpaddltbi  20209  srglmhm  20303  srgrmhm  20304  ringlghm  20395  ringrghm  20396  gsumdixp  20400  dvdsrcl2  20448  crngunit  20460  cntzsubrng  20652  subrgugrp  20676  cntzsubr  20691  rnghmsubcsetclem2  20717  rhmsubcsetclem2  20746  rhmsubcrngclem2  20752  sdrgacs  20882  lmodvsdir  20985  lmodvsass  20986  lmodvsghm  21022  lsssubg  21056  lss1d  21062  islbs2  21256  lidlsubg  21326  lidlsubcl  21327  rngqiprngimfo  21412  lpigen  21472  xrsdsreval  21531  expghm  21594  mulgghm2  21595  ip0r  21756  obs2ss  21848  islindf3  21945  scmatscm  22639  scmataddcl  22642  scmatsubcl  22643  scmatfo  22656  matunit  22804  cpmatelimp  22838  cpmatelimp2  22840  cpmatinvcl  22843  cpmatmcl  22845  mat2pmatf  22854  m2cpmf  22868  cpm2mf  22878  m2cpmfo  22882  m2cpminv  22886  decpmataa0  22894  pm2mpf  22924  pm2mpf1  22925  idpm2idmp  22927  pm2mpfo  22940  elcls2  23200  opnnei  23246  innei  23251  iscnp4  23389  cnpnei  23390  iscncl  23395  cnnei  23408  cnconst  23410  ordthauslem  23509  bwth  23536  1stccnp  23588  llyrest  23611  nllyrest  23612  kgenss  23669  xkoccn  23745  kqsat  23857  kqt0lem  23862  isr0  23863  fbssfi  23963  isfild  23984  filconn  24009  trfilss  24015  fgtr  24016  ufileu  24045  ufilen  24056  fmfnfmlem4  24083  fmfnfm  24084  hausflimi  24106  cnpflf2  24126  cnpflf  24127  cnpfcf  24167  cnextcn  24193  tsmsxplem1  24279  tsmsxp  24281  ustuqtop0  24366  ismeti  24451  isxmet2d  24453  elbl2ps  24515  elbl2  24516  xblpnfps  24521  xblpnf  24522  xbln0  24540  blin  24547  blssexps  24552  blssex  24553  blcls  24632  blsscls  24633  metrest  24650  metustbl  24692  psmetutop  24693  nmf2  24719  ngpi  24754  tngngp3  24782  nmdvr  24796  nmoi  24854  nmoix  24855  nmoleub  24857  nghmcn  24871  iccntr  24948  metdsle  24979  icoopnst  25067  iocopnst  25068  icccvx  25078  pi1xfr  25183  isclmi0  25226  iscvsi  25257  cphipval  25371  lmmbr  25386  lmmbr2  25387  iscfil3  25401  iscau2  25405  cfilres  25424  bcthlem1  25452  bcthlem4  25455  bcthlem5  25456  rrxmet  25536  ioombl  25693  iccvolcl  25695  ioovolcl  25698  mbfi1fseqlem3  25845  mbfi1fseqlem4  25846  mbfi1fseqlem5  25847  ig1pcl  26305  ig1prsp  26307  aannenlem1  26458  taylplem1  26492  dvtaylp  26499  relogeftb  26715  logdivlt  26752  cxpexp  26799  rpcxpcl  26807  isppw2  27245  vmappw  27246  lgslem4  27430  lgscllem  27434  lgsneg1  27452  lgsne0  27465  nosepdm  27814  sltsdisj  27962  mulcutlem  28290  ltonold  28420  zsoring  28568  bdayfinbndlem1  28626  z12bdaylem  28643  brbtwn2  29196  ax5seglem1  29219  ax5seglem2  29220  axcontlem4  29258  ewlkprop  29894  uspgr2wlkeq  29936  uhgrwkspthlem2  30044  clwlkclwwlkfo  30301  eupth2lem3lem7  30526  frgr3vlem2  30566  3cyclfrgrrn1  30577  4cycl2vnunb  30582  frgrncvvdeqlem8  30598  grpoidinvlem3  30799  isvciOLD  30873  nmcvcn  30988  ipval2lem2  30997  sspimsval  31031  isblo2  31076  nmoo0  31084  blocni  31098  isph  31115  hvadd4  31329  hiassdi  31384  ocsh  31576  chj4  31828  spansncol  31861  pjjsi  31993  hoscl  32038  hodcl  32040  hoadd4  32077  homco1  32094  homulass  32095  hoadddi  32096  hoadddir  32097  unoplin  32213  adjvalval  32230  hmoplin  32235  bralnfn  32241  brafnmul  32244  lnopmi  32293  lnopcoi  32296  hmops  32313  hmopm  32314  nmophmi  32324  lnfncnbd  32350  cnlnadjlem2  32361  adjlnop  32379  adjmul  32385  adjadd  32386  branmfn  32398  kbass5  32413  kbass6  32414  leop2  32417  leopadd  32425  leopmuli  32426  pjimai  32469  atcvatlem  32678  chirredlem2  32684  mdsymlem3  32698  mdsymlem5  32700  sumdmdii  32708  sumdmdlem  32711  cdj3lem2a  32729  cdj3lem2b  32730  cdj3lem3a  32732  cdj3i  32734  nn0difffzod  33090  xreceu  33182  cshwrnid  33222  toslublem  33233  tosglblem  33235  lmodvslmhm  33311  archiabllem1b  33453  archiabllem2c  33456  archiabl  33459  slmdvsdir  33477  slmdvsass  33478  grplsm0l  33656  pidlnzb  33674  rprmndvdsru  33764  mplvrpmmhm  33881  mplvrpmrhm  33882  zarcls1  34204  pstmxmet  34232  ordtconnlem1  34259  hasheuni  34420  omsf  34631  ballotlemirc  34867  signswmnd  34889  bnj1204  35345  fineqvac  35462  fisshasheq  35539  revpfxsfxrev  35540  txpconn  35657  cvmscld  35698  satfbrsuc  35791  satfrnmapom  35795  satfun  35836  elmpps  35998  dfrdg2  36218  wsuclem  36248  segconeu  36436  linecom  36575  linethru  36578  lineintmo  36582  fnemeet2  36801  fnejoin2  36803  fvineqsneq  37980  lindsadd  38186  lindsdom  38187  lindsenlbs  38188  matunitlindflem1  38189  matunitlindflem2  38190  heicant  38228  mblfinlem1  38230  mblfinlem3  38232  ismblfin  38234  cnambfre  38241  itg2addnclem2  38245  ftc1anclem1  38266  ftc1anclem5  38270  ftc1anclem6  38271  ftc2nc  38275  areacirclem2  38282  areacirclem4  38284  areacirclem5  38285  areacirc  38286  fzmul  38314  subspopn  38325  isbndx  38355  isbnd2  38356  isbnd3  38357  ssbnd  38361  prdstotbnd  38367  heibor1  38383  rrnmet  38402  rngonegmn1l  38514  rngohomco  38547  rngoisocnv  38554  rngoisoco  38555  crngohomfo  38579  isidlc  38588  rngoidl  38597  prnc  38640  ispridlc  38643  cvrval2  39972  glbconxN  40076  hlrelat5N  40099  cvratlem  40119  cvrat2  40127  athgt  40154  3dim2  40166  llnn0  40214  lplnn0N  40245  lvoln0N  40289  snatpsubN  40448  paddasslem18  40535  pmod1i  40546  lhpexle2  40708  lhpexle3lem  40709  lhpexle3  40710  ldilcnv  40813  trlcnv  40863  trlnidatb  40875  cdleme32snaw  41133  cdleme32fvaw  41137  cdleme42ke  41183  cdlemeg46gf  41231  cdleme50trn12  41250  cdlemg1cex  41286  cdlemb3  41304  tgrpgrplem  41447  tgrpabl  41449  tendoplcl2  41476  tendo0pl  41489  tendoicl  41494  tendoipl  41495  cdlemkid3N  41631  tendoex  41673  erngdvlem4  41689  erngdvlem4-rN  41697  dib1dim  41863  dib1dim2  41866  dihglbcpreN  41998  dihmeetALTN  42025  dih1dimatlem  42027  dihatlat  42032  lcmineqlem1  42720  lcmineqlem3  42722  aks4d1p1  42767  aks4d1p7d1  42773  aks4d1p8  42778  sticksstones1  42837  sticksstones2  42838  sticksstones3  42839  sticksstones8  42844  sticksstones10  42846  sticksstones11  42847  sticksstones12a  42848  sticksstones12  42849  sticksstones17  42854  sticksstones19  42856  oddcomabszz  43597  acongtr  43631  rpnnen3lem  43684  islssfg  43723  lmhmfgsplit  43739  unxpwdom3  43748  hbtlem7  43778  iocmbl  43866  ss2iundf  44311  ismnu  44897  grumnudlem  44921  ismnushort  44937  nzss  44953  dvconstbi  44970  bccbc  44981  uzmptshftfval  44982  iccdifprioo  46158  climisp  46386  limsupresxr  46406  liminfresxr  46407  dvnmul  46583  volico  46623  volioore  46630  fourierdlem74  46820  fourierdlem75  46821  sge0iunmptlemfi  47053  sge0iunmptlemre  47055  sge0iunmpt  47058  sge0xp  47069  hspmbllem2  47267  smflimlem3  47413  smfsupmpt  47455  smfinflem  47457  smfinfmpt  47459  smflimsupmpt  47469  smfliminfmpt  47472  funressnbrafv2  47904  uniimaelsetpreimafv  48068  imasetpreimafvbijlemfv1  48075  imasetpreimafvbijlemfo  48077  sprsymrelfo  48169  nnsum4primesodd  48484  nnsum4primesoddALTV  48485  grtrissvtx  48632  gricgrlic  48706  nn0mnd  48867  lcoss  49135  snlindsntorlem  49169  mreclat  49694  aacllem  50509