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  9073  findcard  9090  enfii  9112  domtrfil  9118  domnsymfi  9126  phplem2  9131  php  9133  wemaplem3  9455  en2eqpr  9919  infxpabs  10123  infxp  10126  cfflb  10171  cfsmolem  10182  isf32lem12  10276  fin1a2lem9  10320  fin1a2s  10326  axcc3  10350  axdc3lem4  10365  zornn0g  10417  pwfseqlem4  10575  tskwun  10697  tskint  10698  tskxp  10700  tskmap  10701  gruf  10724  grutsk1  10734  addcanpi  10812  ltapi  10816  mul4  11303  add4  11356  2addsub  11396  addsubeq4  11397  muladd  11571  ltleadd  11622  receu  11784  p1le  11988  mulgt1  12005  lbinf  12097  zdiv  12564  fzind  12592  fnn0ind  12593  fzindd  12596  uzss  12776  zbtwnre  12861  qmulcl  12882  qreccl  12884  xrlttr  13056  xaddass  13166  xmulasslem3  13203  xadddilem  13211  xrsupsslem  13224  xrinfmsslem  13225  supxrunb1  13236  ioo0  13288  ico0  13309  ioc0  13310  icc0  13311  iooshf  13344  prunioo  13399  ioojoin  13401  elfz5  13434  elfz0fzfz0  13551  elfzonelfzo  13687  fzind2  13706  modaddb  13831  mulexpz  14027  expsub  14035  digit1  14162  facndiv  14213  faclbnd4lem4  14221  faclbnd4  14222  faclbnd5  14223  bccmpl  14234  bcval5  14243  bcpasc  14246  hashunx  14311  hashunsnggt  14319  hashdmpropge2  14408  ccatrn  14515  swrdspsleq  14591  swrdccat2  14595  ccatpfx  14626  pfxccat1  14627  swrdswrd  14630  cshf1  14735  crim  15040  absmax  15255  ello12r  15442  elo12r  15453  climshftlem  15499  2sumeq2dv  15630  hash2iun  15748  expcnv  15789  2cprodeq2dv  15850  rpnnen2lem7  16147  dvdsval3  16185  dvdsnegb  16202  muldvds1  16209  muldvds2  16210  dvdscmul  16211  dvdsmulc  16212  dvdsmulcr  16214  dvds2ln  16218  divalgb  16333  ndvdssub  16338  gcddiv  16480  lcmfval  16550  lcmfcl  16557  dvdslcmf  16560  rpexp1i  16652  phiprmpw  16705  hashgcdeq  16719  pythagtriplem1  16746  pockthg  16836  infpnlem1  16840  4sqlem3  16880  0ramcl  16953  firest  17354  imasaddfnlem  17451  imasleval  17464  mrerintcl  17518  iscatd  17598  fullestrcsetc  18076  fullsetcestrc  18091  clatleglb  18443  mreclatBAD  18488  pslem  18497  mndind  18755  grplmulf1o  18945  grplactcnv  18975  mulgnn0subcl  19019  mulgsubcl  19020  mulgdir  19038  issubg2  19073  issubgrpd2  19074  nmzsubg  19096  eqgen  19112  cycsubm  19133  cycsubgcl  19137  cycsubgss  19138  ghmmulg  19159  ghmf1  19177  kerf1ghm  19178  conjghm  19180  symgpssefmnd  19327  gsmsymgreqlem2  19362  symgfixfo  19370  odeq  19481  odval2  19482  odf1  19493  dfod2  19495  gexdvds  19515  gexdvds2  19516  gexcl2  19520  gexdvds3  19521  sylow2blem2  19552  efgsp1  19668  efgrelexlemb  19681  cmnbascntr  19736  mulgmhm  19758  mulgghm  19759  iscyggen2  19812  iscyg3  19817  ablsimpgfindlem1  20040  ogrpaddltbi  20070  srglmhm  20158  srgrmhm  20159  ringlghm  20249  ringrghm  20250  gsumdixp  20256  dvdsrcl2  20304  crngunit  20316  cntzsubrng  20502  subrgugrp  20526  cntzsubr  20541  rnghmsubcsetclem2  20567  rhmsubcsetclem2  20596  rhmsubcrngclem2  20602  sdrgacs  20736  lmodvsdir  20839  lmodvsass  20840  lmodvsghm  20876  lsssubg  20910  lss1d  20916  islbs2  21111  lidlsubg  21180  lidlsubcl  21181  rngqiprngimfo  21258  lpigen  21292  xrsdsreval  21368  expghm  21432  mulgghm2  21433  ip0r  21594  obs2ss  21686  islindf3  21783  scmatscm  22459  scmataddcl  22462  scmatsubcl  22463  scmatfo  22476  matunit  22624  cpmatelimp  22658  cpmatelimp2  22660  cpmatinvcl  22663  cpmatmcl  22665  mat2pmatf  22674  m2cpmf  22688  cpm2mf  22698  m2cpmfo  22702  m2cpminv  22706  decpmataa0  22714  pm2mpf  22744  pm2mpf1  22745  idpm2idmp  22747  pm2mpfo  22760  elcls2  23020  opnnei  23066  innei  23071  iscnp4  23209  cnpnei  23210  iscncl  23215  cnnei  23228  cnconst  23230  ordthauslem  23329  bwth  23356  1stccnp  23408  llyrest  23431  nllyrest  23432  kgenss  23489  xkoccn  23565  kqsat  23677  kqt0lem  23682  isr0  23683  fbssfi  23783  isfild  23804  filconn  23829  trfilss  23835  fgtr  23836  ufileu  23865  ufilen  23876  fmfnfmlem4  23903  fmfnfm  23904  hausflimi  23926  cnpflf2  23946  cnpflf  23947  cnpfcf  23987  cnextcn  24013  tsmsxplem1  24099  tsmsxp  24101  ustuqtop0  24186  ismeti  24271  isxmet2d  24273  elbl2ps  24335  elbl2  24336  xblpnfps  24341  xblpnf  24342  xbln0  24360  blin  24367  blssexps  24372  blssex  24373  blcls  24452  blsscls  24453  metrest  24470  metustbl  24512  psmetutop  24513  nmf2  24539  ngpi  24574  tngngp3  24602  nmdvr  24616  nmoi  24674  nmoix  24675  nmoleub  24677  nghmcn  24691  iccntr  24768  metdsle  24799  icoopnst  24894  iocopnst  24895  icccvx  24906  pi1xfr  25013  isclmi0  25056  iscvsi  25087  cphipval  25201  lmmbr  25216  lmmbr2  25217  iscfil3  25231  iscau2  25235  cfilres  25254  bcthlem1  25282  bcthlem4  25285  bcthlem5  25286  rrxmet  25366  ioombl  25524  iccvolcl  25526  ioovolcl  25529  mbfi1fseqlem3  25676  mbfi1fseqlem4  25677  mbfi1fseqlem5  25678  ig1pcl  26142  ig1prsp  26144  aannenlem1  26294  taylplem1  26328  dvtaylp  26336  relogeftb  26551  logdivlt  26588  cxpexp  26635  rpcxpcl  26643  isppw2  27083  vmappw  27084  lgslem4  27269  lgscllem  27273  lgsneg1  27291  lgsne0  27304  nosepdm  27654  sltsdisj  27801  mulcutlem  28129  ltonold  28259  zsoring  28407  bdayfinbndlem1  28465  z12bdaylem  28482  brbtwn2  28980  ax5seglem1  29003  ax5seglem2  29004  axcontlem4  29042  ewlkprop  29679  uspgr2wlkeq  29721  uhgrwkspthlem2  29829  clwlkclwwlkfo  30086  eupth2lem3lem7  30311  frgr3vlem2  30351  3cyclfrgrrn1  30362  4cycl2vnunb  30367  frgrncvvdeqlem8  30383  grpoidinvlem3  30583  isvciOLD  30657  nmcvcn  30772  ipval2lem2  30781  sspimsval  30815  isblo2  30860  nmoo0  30868  blocni  30882  isph  30899  hvadd4  31113  hiassdi  31168  ocsh  31360  chj4  31612  spansncol  31645  pjjsi  31777  hoscl  31822  hodcl  31824  hoadd4  31861  homco1  31878  homulass  31879  hoadddi  31880  hoadddir  31881  unoplin  31997  adjvalval  32014  hmoplin  32019  bralnfn  32025  brafnmul  32028  lnopmi  32077  lnopcoi  32080  hmops  32097  hmopm  32098  nmophmi  32108  lnfncnbd  32134  cnlnadjlem2  32145  adjlnop  32163  adjmul  32169  adjadd  32170  branmfn  32182  kbass5  32197  kbass6  32198  leop2  32201  leopadd  32209  leopmuli  32210  pjimai  32253  atcvatlem  32462  chirredlem2  32468  mdsymlem3  32482  mdsymlem5  32484  sumdmdii  32492  sumdmdlem  32495  cdj3lem2a  32513  cdj3lem2b  32514  cdj3lem3a  32516  cdj3i  32518  nn0difffzod  32886  xreceu  33005  cshwrnid  33045  toslublem  33056  tosglblem  33058  lmodvslmhm  33135  archiabllem1b  33276  archiabllem2c  33279  archiabl  33282  slmdvsdir  33300  slmdvsass  33301  grplsm0l  33486  pidlnzb  33505  rprmndvdsru  33612  mplvrpmmhm  33713  mplvrpmrhm  33714  zarcls1  34028  pstmxmet  34056  ordtconnlem1  34083  hasheuni  34244  omsf  34455  ballotlemirc  34691  signswmnd  34716  bnj1204  35170  fineqvac  35274  fisshasheq  35311  revpfxsfxrev  35312  txpconn  35428  cvmscld  35469  satfbrsuc  35562  satfrnmapom  35566  satfun  35607  elmpps  35769  dfrdg2  35989  wsuclem  36019  segconeu  36207  linecom  36346  linethru  36349  lineintmo  36353  fnemeet2  36563  fnejoin2  36565  fvineqsneq  37619  lindsadd  37816  lindsdom  37817  lindsenlbs  37818  matunitlindflem1  37819  matunitlindflem2  37820  heicant  37858  mblfinlem1  37860  mblfinlem3  37862  ismblfin  37864  cnambfre  37871  itg2addnclem2  37875  ftc1anclem1  37896  ftc1anclem5  37900  ftc1anclem6  37901  ftc2nc  37905  areacirclem2  37912  areacirclem4  37914  areacirclem5  37915  areacirc  37916  fzmul  37944  subspopn  37955  isbndx  37985  isbnd2  37986  isbnd3  37987  ssbnd  37991  prdstotbnd  37997  heibor1  38013  rrnmet  38032  rngonegmn1l  38144  rngohomco  38177  rngoisocnv  38184  rngoisoco  38185  crngohomfo  38209  isidlc  38218  rngoidl  38227  prnc  38270  ispridlc  38273  cvrval2  39556  glbconxN  39660  hlrelat5N  39683  cvratlem  39703  cvrat2  39711  athgt  39738  3dim2  39750  llnn0  39798  lplnn0N  39829  lvoln0N  39873  snatpsubN  40032  paddasslem18  40119  pmod1i  40130  lhpexle2  40292  lhpexle3lem  40293  lhpexle3  40294  ldilcnv  40397  trlcnv  40447  trlnidatb  40459  cdleme32snaw  40717  cdleme32fvaw  40721  cdleme42ke  40767  cdlemeg46gf  40815  cdleme50trn12  40834  cdlemg1cex  40870  cdlemb3  40888  tgrpgrplem  41031  tgrpabl  41033  tendoplcl2  41060  tendo0pl  41073  tendoicl  41078  tendoipl  41079  cdlemkid3N  41215  tendoex  41257  erngdvlem4  41273  erngdvlem4-rN  41281  dib1dim  41447  dib1dim2  41450  dihglbcpreN  41582  dihmeetALTN  41609  dih1dimatlem  41611  dihatlat  41616  lcmineqlem1  42305  lcmineqlem3  42307  aks4d1p1  42352  aks4d1p7d1  42358  aks4d1p8  42363  sticksstones1  42422  sticksstones2  42423  sticksstones3  42424  sticksstones8  42429  sticksstones10  42431  sticksstones11  42432  sticksstones12a  42433  sticksstones12  42434  sticksstones17  42439  sticksstones19  42441  oddcomabszz  43207  acongtr  43241  rpnnen3lem  43294  islssfg  43333  lmhmfgsplit  43349  unxpwdom3  43358  hbtlem7  43388  iocmbl  43476  ss2iundf  43921  ismnu  44523  grumnudlem  44547  ismnushort  44563  nzss  44579  dvconstbi  44596  bccbc  44607  uzmptshftfval  44608  iccdifprioo  45783  climisp  46011  limsupresxr  46031  liminfresxr  46032  dvnmul  46208  volico  46248  volioore  46255  fourierdlem74  46445  fourierdlem75  46446  sge0iunmptlemfi  46678  sge0iunmptlemre  46680  sge0iunmpt  46683  sge0xp  46694  hspmbllem2  46892  smflimlem3  47038  smfsupmpt  47080  smfinflem  47082  smfinfmpt  47084  smflimsupmpt  47094  smfliminfmpt  47097  funressnbrafv2  47511  uniimaelsetpreimafv  47663  imasetpreimafvbijlemfv1  47670  imasetpreimafvbijlemfo  47672  sprsymrelfo  47764  nnsum4primesodd  48063  nnsum4primesoddALTV  48064  grtrissvtx  48211  gricgrlic  48285  nn0mnd  48446  lcoss  48703  snlindsntorlem  48737  mreclat  49263  aacllem  50067