Theorem 3expa 1098

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-3an 1070

This theorem is referenced by:  3exp  1099  ad4ant123  1152  ad4ant124  1153  ad4ant134  1154  ad4ant234  1155  ad5ant123  1344  3anidm23  1401  mp3an2  1428  mpd3an3  1441  rgen3  3148  vtocl3  3476  spc3egv  3516  moi2  3617  sbc3ie  3751  2if2  4397  preq12bg  4652  ralxfrd2  5160  reuhypd  5170  otsndisj  5258  funcnvqp  6245  fvtp1g  6781  fntpb  6792  f1imass  6841  weisoeq  6925  f1ofveu  6965  f1ocnvfv3  6966  curry1f  7602  curry2f  7604  funsssuppss  7652  tfrlem11  7821  oalimcl  7979  oeordsuc  8013  oelim2  8014  nneob  8071  mapxpen  8471  findcard  8544  wemaplem3  8799  en2eqpr  9219  infxpabs  9424  infxp  9427  cfflb  9471  cfsmolem  9482  isf32lem12  9576  fin1a2lem9  9620  fin1a2s  9626  axcc3  9650  axdc3lem4  9665  zornn0g  9717  pwfseqlem4  9874  tskwun  9996  tskint  9997  tskxp  9999  tskmap  10000  gruf  10023  grutsk1  10033  addcanpi  10111  ltapi  10115  mul4  10600  add4  10652  2addsub  10693  addsubeq4  10694  muladd  10865  ltleadd  10916  receu  11078  p1le  11278  lbinf  11387  zdiv  11858  fzind  11886  fnn0ind  11887  uzss  12072  zbtwnre  12153  qmulcl  12174  qreccl  12176  xrlttr  12343  xaddass  12451  xmulasslem3  12488  xadddilem  12496  xrsupsslem  12509  xrinfmsslem  12510  supxrunb1  12521  ioo0  12572  ico0  12593  ioc0  12594  icc0  12595  iooshf  12624  prunioo  12676  ioojoin  12678  elfz5  12709  elfz0fzfz0  12821  elfzonelfzo  12947  fzind2  12963  mulexpz  13277  expsub  13285  digit1  13406  facndiv  13456  faclbnd4lem4  13464  faclbnd4  13465  faclbnd5  13466  bccmpl  13477  bcval5  13486  bcpasc  13489  hashunx  13553  hashdmpropge2  13642  ccatrn  13742  swrdccat1OLD  13840  swrdccat2  13841  pfxccat1  13874  swrdswrd  13877  cats1un  13904  cshf1  14024  crim  14325  absmax  14540  ello12r  14725  elo12r  14736  climshftlem  14782  2sumeq2dv  14912  hash2iun  15028  expcnv  15069  2cprodeq2dv  15129  rpnnen2lem7  15423  dvdsval3  15461  dvdsnegb  15477  muldvds1  15484  muldvds2  15485  dvdscmul  15486  dvdsmulc  15487  dvdsmulcr  15489  dvds2ln  15492  divalgb  15605  ndvdssub  15610  gcddiv  15745  lcmfval  15811  lcmfcl  15818  dvdslcmf  15821  rpexp1i  15911  phiprmpw  15959  hashgcdeq  15972  pythagtriplem1  15999  pockthg  16088  infpnlem1  16092  4sqlem3  16132  0ramcl  16205  firest  16552  imasaddfnlem  16647  imasleval  16660  xpsfrn2  16689  mrerintcl  16716  iscatd  16792  fullestrcsetc  17249  fullsetcestrc  17264  clatleglb  17584  mreclatBAD  17645  pslem  17664  mndind  17824  grplmulf1o  17950  grplactcnv  17979  mulgnn0subcl  18016  mulgsubcl  18017  mulgdir  18033  issubg2  18068  issubgrpd2  18069  cycsubgcl  18079  cycsubgss  18080  nmzsubg  18094  eqgen  18106  ghmmulg  18131  conjghm  18150  symgfixfo  18318  odeq  18430  odval2  18431  odf1  18440  dfod2  18442  gexdvds  18460  gexdvds2  18461  gexcl2  18465  gexdvds3  18466  sylow2blem2  18497  efgsp1  18611  efgrelexlemb  18626  mulgmhm  18696  mulgghm  18697  iscyggen2  18746  iscyg3  18751  srglmhm  18998  srgrmhm  18999  ringlghm  19067  ringrghm  19068  gsumdixp  19072  dvdsrcl2  19113  crngunit  19125  kerf1ghm  19210  kerf1hrmOLD  19211  subrgugrp  19267  cntzsubr  19280  sdrgacs  19292  lmodvsdir  19370  lmodvsass  19371  lmodvsghm  19407  lsssubg  19441  lss1d  19447  islbs2  19638  lidlsubg  19699  lidlsubcl  19700  quscrng  19724  lpigen  19740  xrsdsreval  20282  expghm  20335  mulgghm2  20336  ip0r  20473  obs2ss  20565  islindf3  20662  scmatscm  20816  scmataddcl  20819  scmatsubcl  20820  scmatfo  20833  matunit  20981  cpmatelimp  21014  cpmatelimp2  21016  cpmatinvcl  21019  cpmatmcl  21021  mat2pmatf  21030  m2cpmf  21044  cpm2mf  21054  m2cpmfo  21058  m2cpminv  21062  decpmataa0  21070  pm2mpf  21100  pm2mpf1  21101  idpm2idmp  21103  pm2mpfo  21116  elcls2  21376  opnnei  21422  innei  21427  iscnp4  21565  cnpnei  21566  iscncl  21571  cnnei  21584  cnconst  21586  ordthauslem  21685  bwth  21712  1stccnp  21764  llyrest  21787  nllyrest  21788  kgenss  21845  xkoccn  21921  kqsat  22033  kqt0lem  22038  isr0  22039  fbssfi  22139  isfild  22160  filconn  22185  trfilss  22191  fgtr  22192  ufileu  22221  ufilen  22232  fmfnfmlem4  22259  fmfnfm  22260  hausflimi  22282  cnpflf2  22302  cnpflf  22303  cnpfcf  22343  cnextcn  22369  tsmsxplem1  22454  tsmsxp  22456  ustuqtop0  22542  ismeti  22628  isxmet2d  22630  elbl2ps  22692  elbl2  22693  xblpnfps  22698  xblpnf  22699  xbln0  22717  blin  22724  blssexps  22729  blssex  22730  blcls  22809  blsscls  22810  metrest  22827  metustbl  22869  psmetutop  22870  nmf2  22895  ngpi  22930  tngngp3  22958  nmdvr  22972  nmoi  23030  nmoix  23031  nmoleub  23033  nghmcn  23047  iccntr  23122  metdsle  23153  icoopnst  23236  iocopnst  23237  icccvx  23247  pi1xfr  23352  isclmi0  23395  iscvsi  23426  cphipval  23539  lmmbr  23554  lmmbr2  23555  iscfil3  23569  iscau2  23573  cfilres  23592  bcthlem1  23620  bcthlem4  23623  bcthlem5  23624  rrxmet  23704  ioombl  23859  iccvolcl  23861  ioovolcl  23864  mbfi1fseqlem3  24011  mbfi1fseqlem4  24012  mbfi1fseqlem5  24013  ig1pcl  24462  ig1prsp  24464  aannenlem1  24610  taylplem1  24644  dvtaylp  24651  relogeftb  24859  logdivlt  24895  cxpexp  24942  rpcxpcl  24950  isppw2  25384  vmappw  25385  lgslem4  25568  lgscllem  25572  lgsneg1  25590  lgsne0  25603  brbtwn2  26384  ax5seglem1  26407  ax5seglem2  26408  axcontlem4  26446  ewlkprop  27078  uspgr2wlkeq  27120  uhgrwkspthlem2  27233  clwlkclwwlkfoOLD  27509  clwlkclwwlkfo  27513  eupth2lem3lem7  27754  frgr3vlem2  27798  3cyclfrgrrn1  27809  4cycl2vnunb  27814  frgrncvvdeqlem8  27830  grpoidinvlem3  28050  isvciOLD  28124  nmcvcn  28239  ipval2lem2  28248  sspimsval  28282  isblo2  28327  nmoo0  28335  blocni  28349  isph  28366  sspphOLD  28399  hvadd4  28582  hiassdi  28637  ocsh  28831  chj4  29083  spansncol  29116  pjjsi  29248  hoscl  29293  hodcl  29295  hoadd4  29332  homco1  29349  homulass  29350  hoadddi  29351  hoadddir  29352  unoplin  29468  adjvalval  29485  hmoplin  29490  bralnfn  29496  brafnmul  29499  lnopmi  29548  lnopcoi  29551  hmops  29568  hmopm  29569  nmophmi  29579  lnfncnbd  29605  cnlnadjlem2  29616  adjlnop  29634  adjmul  29640  adjadd  29641  branmfn  29653  kbass5  29668  kbass6  29669  leop2  29672  leopadd  29680  leopmuli  29681  pjimai  29724  atcvatlem  29933  chirredlem2  29939  mdsymlem3  29953  mdsymlem5  29955  sumdmdii  29963  sumdmdlem  29966  cdj3lem2a  29984  cdj3lem2b  29985  cdj3lem3a  29987  cdj3i  29989  xreceu  30333  toslublem  30364  tosglblem  30366  ogrpaddltbi  30416  archiabllem1b  30443  archiabllem2c  30446  archiabl  30449  slmdvsdir  30466  slmdvsass  30467  lmodvslmhm  30483  pstmxmet  30738  ordtconnlem1  30768  hasheuni  30945  omsf  31156  ballotlemirc  31392  signswmnd  31434  bnj1204  31890  txpconn  32024  cvmscld  32065  elmpps  32280  dfrdg2  32501  wsuclem  32573  frrlem13  32596  nosepdm  32649  segconeu  32933  linecom  33072  linethru  33075  lineintmo  33079  fnemeet2  33176  fnejoin2  33178  fvineqsneq  34069  lindsadd  34274  lindsdom  34275  lindsenlbs  34276  matunitlindflem1  34277  matunitlindflem2  34278  heicant  34316  mblfinlem1  34318  mblfinlem3  34320  ismblfin  34322  cnambfre  34329  itg2addnclem2  34333  ftc1anclem1  34356  ftc1anclem5  34360  ftc1anclem6  34361  ftc2nc  34365  areacirclem2  34372  areacirclem4  34374  areacirclem5  34375  areacirc  34376  fzmul  34406  subspopn  34417  isbndx  34450  isbnd2  34451  isbnd3  34452  ssbnd  34456  prdstotbnd  34462  heibor1  34478  rrnmet  34497  rngonegmn1l  34609  rngohomco  34642  rngoisocnv  34649  rngoisoco  34650  crngohomfo  34674  isidlc  34683  rngoidl  34692  prnc  34735  ispridlc  34738  cvrval2  35803  glbconxN  35907  hlrelat5N  35930  cvratlem  35950  cvrat2  35958  athgt  35985  3dim2  35997  llnn0  36045  lplnn0N  36076  lvoln0N  36120  snatpsubN  36279  paddasslem18  36366  pmod1i  36377  lhpexle2  36539  lhpexle3lem  36540  lhpexle3  36541  ldilcnv  36644  trlcnv  36694  trlnidatb  36706  cdleme32snaw  36964  cdleme32fvaw  36968  cdleme42ke  37014  cdlemeg46gf  37062  cdleme50trn12  37081  cdlemg1cex  37117  cdlemb3  37135  tgrpgrplem  37278  tgrpabl  37280  tendoplcl2  37307  tendo0pl  37320  tendoicl  37325  tendoipl  37326  cdlemkid3N  37462  tendoex  37504  erngdvlem4  37520  erngdvlem4-rN  37528  dib1dim  37694  dib1dim2  37697  dihglbcpreN  37829  dihmeetALTN  37856  dih1dimatlem  37858  dihatlat  37863  oddcomabszz  38882  acongtr  38916  rpnnen3lem  38969  islssfg  39011  lmhmfgsplit  39027  unxpwdom3  39036  hbtlem7  39066  iocmbl  39160  ss2iundf  39312  ismnu  39917  grumnudlem  39941  ablsimpgfindlem1  39988  nzss  40009  dvconstbi  40026  bccbc  40037  uzmptshftfval  40038  iccdifprioo  41169  climisp  41404  limsupresxr  41424  liminfresxr  41425  dvnmul  41604  volico  41645  volioore  41652  fourierdlem74  41842  fourierdlem75  41843  sge0iunmptlemfi  42072  sge0iunmptlemre  42074  sge0iunmpt  42077  sge0xp  42088  hspmbllem2  42286  smflimlem3  42426  smfsupmpt  42466  smfinflem  42468  smfinfmpt  42470  smflimsupmpt  42480  smfliminfmpt  42483  funressnbrafv2  42795  sprsymrelfo  42967  nnsum4primesodd  43269  nnsum4primesoddALTV  43270  rnghmsubcsetclem2  43551  rhmsubcsetclem2  43597  rhmsubcrngclem2  43603  lcoss  43798  snlindsntorlem  43832  aacllem  44209