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  3181  vtocl3  3523  spc3egv  3557  moi2  3674  sbc3ie  3818  2if2  4535  preq12bg  4809  ralxfrd2  5357  reuhypd  5364  otsndisj  5467  funcnvqp  6556  fvtp1g  7144  fntpb  7155  f1imass  7210  weisoeq  7301  f1ofveu  7352  f1ocnvfv3  7353  funeldmdif  7992  curry1f  8048  curry2f  8050  funsssuppss  8132  frrlem13  8240  tfrlem11  8319  oalimcl  8487  oeordsuc  8522  oelim2  8523  nneob  8584  nadd4  8626  mapxpen  9071  findcard  9088  enfii  9110  domtrfil  9116  domnsymfi  9124  phplem2  9129  php  9131  wemaplem3  9453  en2eqpr  9917  infxpabs  10121  infxp  10124  cfflb  10169  cfsmolem  10180  isf32lem12  10274  fin1a2lem9  10318  fin1a2s  10324  axcc3  10348  axdc3lem4  10363  zornn0g  10415  pwfseqlem4  10573  tskwun  10695  tskint  10696  tskxp  10698  tskmap  10699  gruf  10722  grutsk1  10732  addcanpi  10810  ltapi  10814  mul4  11301  add4  11354  2addsub  11394  addsubeq4  11395  muladd  11569  ltleadd  11620  receu  11782  p1le  11986  mulgt1  12003  lbinf  12095  zdiv  12562  fzind  12590  fnn0ind  12591  fzindd  12594  uzss  12774  zbtwnre  12859  qmulcl  12880  qreccl  12882  xrlttr  13054  xaddass  13164  xmulasslem3  13201  xadddilem  13209  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  iooshf  13342  prunioo  13397  ioojoin  13399  elfz5  13432  elfz0fzfz0  13549  elfzonelfzo  13685  fzind2  13704  modaddb  13829  mulexpz  14025  expsub  14033  digit1  14160  facndiv  14211  faclbnd4lem4  14219  faclbnd4  14220  faclbnd5  14221  bccmpl  14232  bcval5  14241  bcpasc  14244  hashunx  14309  hashunsnggt  14317  hashdmpropge2  14406  ccatrn  14513  swrdspsleq  14589  swrdccat2  14593  ccatpfx  14624  pfxccat1  14625  swrdswrd  14628  cshf1  14733  crim  15038  absmax  15253  ello12r  15440  elo12r  15451  climshftlem  15497  2sumeq2dv  15628  hash2iun  15746  expcnv  15787  2cprodeq2dv  15848  rpnnen2lem7  16145  dvdsval3  16183  dvdsnegb  16200  muldvds1  16207  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  dvdsmulcr  16212  dvds2ln  16216  divalgb  16331  ndvdssub  16336  gcddiv  16478  lcmfval  16548  lcmfcl  16555  dvdslcmf  16558  rpexp1i  16650  phiprmpw  16703  hashgcdeq  16717  pythagtriplem1  16744  pockthg  16834  infpnlem1  16838  4sqlem3  16878  0ramcl  16951  firest  17352  imasaddfnlem  17449  imasleval  17462  mrerintcl  17516  iscatd  17596  fullestrcsetc  18074  fullsetcestrc  18089  clatleglb  18441  mreclatBAD  18486  pslem  18495  mndind  18753  grplmulf1o  18943  grplactcnv  18973  mulgnn0subcl  19017  mulgsubcl  19018  mulgdir  19036  issubg2  19071  issubgrpd2  19072  nmzsubg  19094  eqgen  19110  cycsubm  19131  cycsubgcl  19135  cycsubgss  19136  ghmmulg  19157  ghmf1  19175  kerf1ghm  19176  conjghm  19178  symgpssefmnd  19325  gsmsymgreqlem2  19360  symgfixfo  19368  odeq  19479  odval2  19480  odf1  19491  dfod2  19493  gexdvds  19513  gexdvds2  19514  gexcl2  19518  gexdvds3  19519  sylow2blem2  19550  efgsp1  19666  efgrelexlemb  19679  cmnbascntr  19734  mulgmhm  19756  mulgghm  19757  iscyggen2  19810  iscyg3  19815  ablsimpgfindlem1  20038  ogrpaddltbi  20068  srglmhm  20156  srgrmhm  20157  ringlghm  20247  ringrghm  20248  gsumdixp  20254  dvdsrcl2  20302  crngunit  20314  cntzsubrng  20500  subrgugrp  20524  cntzsubr  20539  rnghmsubcsetclem2  20565  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  sdrgacs  20734  lmodvsdir  20837  lmodvsass  20838  lmodvsghm  20874  lsssubg  20908  lss1d  20914  islbs2  21109  lidlsubg  21178  lidlsubcl  21179  rngqiprngimfo  21256  lpigen  21290  xrsdsreval  21366  expghm  21430  mulgghm2  21431  ip0r  21592  obs2ss  21684  islindf3  21781  scmatscm  22457  scmataddcl  22460  scmatsubcl  22461  scmatfo  22474  matunit  22622  cpmatelimp  22656  cpmatelimp2  22658  cpmatinvcl  22661  cpmatmcl  22663  mat2pmatf  22672  m2cpmf  22686  cpm2mf  22696  m2cpmfo  22700  m2cpminv  22704  decpmataa0  22712  pm2mpf  22742  pm2mpf1  22743  idpm2idmp  22745  pm2mpfo  22758  elcls2  23018  opnnei  23064  innei  23069  iscnp4  23207  cnpnei  23208  iscncl  23213  cnnei  23226  cnconst  23228  ordthauslem  23327  bwth  23354  1stccnp  23406  llyrest  23429  nllyrest  23430  kgenss  23487  xkoccn  23563  kqsat  23675  kqt0lem  23680  isr0  23681  fbssfi  23781  isfild  23802  filconn  23827  trfilss  23833  fgtr  23834  ufileu  23863  ufilen  23874  fmfnfmlem4  23901  fmfnfm  23902  hausflimi  23924  cnpflf2  23944  cnpflf  23945  cnpfcf  23985  cnextcn  24011  tsmsxplem1  24097  tsmsxp  24099  ustuqtop0  24184  ismeti  24269  isxmet2d  24271  elbl2ps  24333  elbl2  24334  xblpnfps  24339  xblpnf  24340  xbln0  24358  blin  24365  blssexps  24370  blssex  24371  blcls  24450  blsscls  24451  metrest  24468  metustbl  24510  psmetutop  24511  nmf2  24537  ngpi  24572  tngngp3  24600  nmdvr  24614  nmoi  24672  nmoix  24673  nmoleub  24675  nghmcn  24689  iccntr  24766  metdsle  24797  icoopnst  24892  iocopnst  24893  icccvx  24904  pi1xfr  25011  isclmi0  25054  iscvsi  25085  cphipval  25199  lmmbr  25214  lmmbr2  25215  iscfil3  25229  iscau2  25233  cfilres  25252  bcthlem1  25280  bcthlem4  25283  bcthlem5  25284  rrxmet  25364  ioombl  25522  iccvolcl  25524  ioovolcl  25527  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  ig1pcl  26140  ig1prsp  26142  aannenlem1  26292  taylplem1  26326  dvtaylp  26334  relogeftb  26549  logdivlt  26586  cxpexp  26633  rpcxpcl  26641  isppw2  27081  vmappw  27082  lgslem4  27267  lgscllem  27271  lgsneg1  27289  lgsne0  27302  nosepdm  27652  sltsdisj  27799  mulcutlem  28127  ltonold  28257  zsoring  28405  bdayfinbndlem1  28463  z12bdaylem  28480  brbtwn2  28978  ax5seglem1  29001  ax5seglem2  29002  axcontlem4  29040  ewlkprop  29677  uspgr2wlkeq  29719  uhgrwkspthlem2  29827  clwlkclwwlkfo  30084  eupth2lem3lem7  30309  frgr3vlem2  30349  3cyclfrgrrn1  30360  4cycl2vnunb  30365  frgrncvvdeqlem8  30381  grpoidinvlem3  30581  isvciOLD  30655  nmcvcn  30770  ipval2lem2  30779  sspimsval  30813  isblo2  30858  nmoo0  30866  blocni  30880  isph  30897  hvadd4  31111  hiassdi  31166  ocsh  31358  chj4  31610  spansncol  31643  pjjsi  31775  hoscl  31820  hodcl  31822  hoadd4  31859  homco1  31876  homulass  31877  hoadddi  31878  hoadddir  31879  unoplin  31995  adjvalval  32012  hmoplin  32017  bralnfn  32023  brafnmul  32026  lnopmi  32075  lnopcoi  32078  hmops  32095  hmopm  32096  nmophmi  32106  lnfncnbd  32132  cnlnadjlem2  32143  adjlnop  32161  adjmul  32167  adjadd  32168  branmfn  32180  kbass5  32195  kbass6  32196  leop2  32199  leopadd  32207  leopmuli  32208  pjimai  32251  atcvatlem  32460  chirredlem2  32466  mdsymlem3  32480  mdsymlem5  32482  sumdmdii  32490  sumdmdlem  32493  cdj3lem2a  32511  cdj3lem2b  32512  cdj3lem3a  32514  cdj3i  32516  nn0difffzod  32884  xreceu  33003  cshwrnid  33043  toslublem  33054  tosglblem  33056  lmodvslmhm  33133  archiabllem1b  33274  archiabllem2c  33277  archiabl  33280  slmdvsdir  33298  slmdvsass  33299  grplsm0l  33484  pidlnzb  33503  rprmndvdsru  33610  mplvrpmmhm  33711  mplvrpmrhm  33712  zarcls1  34026  pstmxmet  34054  ordtconnlem1  34081  hasheuni  34242  omsf  34453  ballotlemirc  34689  signswmnd  34714  bnj1204  35168  fineqvac  35272  fisshasheq  35309  revpfxsfxrev  35310  txpconn  35426  cvmscld  35467  satfbrsuc  35560  satfrnmapom  35564  satfun  35605  elmpps  35767  dfrdg2  35987  wsuclem  36017  segconeu  36205  linecom  36344  linethru  36347  lineintmo  36351  fnemeet2  36561  fnejoin2  36563  fvineqsneq  37617  lindsadd  37814  lindsdom  37815  lindsenlbs  37816  matunitlindflem1  37817  matunitlindflem2  37818  heicant  37856  mblfinlem1  37858  mblfinlem3  37860  ismblfin  37862  cnambfre  37869  itg2addnclem2  37873  ftc1anclem1  37894  ftc1anclem5  37898  ftc1anclem6  37899  ftc2nc  37903  areacirclem2  37910  areacirclem4  37912  areacirclem5  37913  areacirc  37914  fzmul  37942  subspopn  37953  isbndx  37983  isbnd2  37984  isbnd3  37985  ssbnd  37989  prdstotbnd  37995  heibor1  38011  rrnmet  38030  rngonegmn1l  38142  rngohomco  38175  rngoisocnv  38182  rngoisoco  38183  crngohomfo  38207  isidlc  38216  rngoidl  38225  prnc  38268  ispridlc  38271  cvrval2  39534  glbconxN  39638  hlrelat5N  39661  cvratlem  39681  cvrat2  39689  athgt  39716  3dim2  39728  llnn0  39776  lplnn0N  39807  lvoln0N  39851  snatpsubN  40010  paddasslem18  40097  pmod1i  40108  lhpexle2  40270  lhpexle3lem  40271  lhpexle3  40272  ldilcnv  40375  trlcnv  40425  trlnidatb  40437  cdleme32snaw  40695  cdleme32fvaw  40699  cdleme42ke  40745  cdlemeg46gf  40793  cdleme50trn12  40812  cdlemg1cex  40848  cdlemb3  40866  tgrpgrplem  41009  tgrpabl  41011  tendoplcl2  41038  tendo0pl  41051  tendoicl  41056  tendoipl  41057  cdlemkid3N  41193  tendoex  41235  erngdvlem4  41251  erngdvlem4-rN  41259  dib1dim  41425  dib1dim2  41428  dihglbcpreN  41560  dihmeetALTN  41587  dih1dimatlem  41589  dihatlat  41594  lcmineqlem1  42283  lcmineqlem3  42285  aks4d1p1  42330  aks4d1p7d1  42336  aks4d1p8  42341  sticksstones1  42400  sticksstones2  42401  sticksstones3  42402  sticksstones8  42407  sticksstones10  42409  sticksstones11  42410  sticksstones12a  42411  sticksstones12  42412  sticksstones17  42417  sticksstones19  42419  oddcomabszz  43186  acongtr  43220  rpnnen3lem  43273  islssfg  43312  lmhmfgsplit  43328  unxpwdom3  43337  hbtlem7  43367  iocmbl  43455  ss2iundf  43900  ismnu  44502  grumnudlem  44526  ismnushort  44542  nzss  44558  dvconstbi  44575  bccbc  44586  uzmptshftfval  44587  iccdifprioo  45762  climisp  45990  limsupresxr  46010  liminfresxr  46011  dvnmul  46187  volico  46227  volioore  46234  fourierdlem74  46424  fourierdlem75  46425  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0xp  46673  hspmbllem2  46871  smflimlem3  47017  smfsupmpt  47059  smfinflem  47061  smfinfmpt  47063  smflimsupmpt  47073  smfliminfmpt  47076  funressnbrafv2  47490  uniimaelsetpreimafv  47642  imasetpreimafvbijlemfv1  47649  imasetpreimafvbijlemfo  47651  sprsymrelfo  47743  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  grtrissvtx  48190  gricgrlic  48264  nn0mnd  48425  lcoss  48682  snlindsntorlem  48716  mreclat  49242  aacllem  50046