Theorem 3expa 1119

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3exp  1120  ad4ant123  1174  ad4ant124  1175  ad4ant134  1176  ad4ant234  1177  ad5ant123  1367  3anidm23  1424  mp3an2  1452  mpd3an3  1465  rgen3  3182  vtocl3  3511  spc3egv  3545  moi2  3662  sbc3ie  3806  2if2  4522  preq12bg  4796  ralxfrd2  5354  reuhypd  5361  otsndisj  5473  funcnvqp  6562  fvtp1g  7153  fntpb  7164  f1imass  7219  weisoeq  7310  f1ofveu  7361  f1ocnvfv3  7362  funeldmdif  8001  curry1f  8056  curry2f  8058  funsssuppss  8140  frrlem13  8248  tfrlem11  8327  oalimcl  8495  oeordsuc  8530  oelim2  8531  nneob  8592  nadd4  8634  mapxpen  9081  findcard  9098  enfii  9120  domtrfil  9126  domnsymfi  9134  phplem2  9139  php  9141  wemaplem3  9463  en2eqpr  9929  infxpabs  10133  infxp  10136  cfflb  10181  cfsmolem  10192  isf32lem12  10286  fin1a2lem9  10330  fin1a2s  10336  axcc3  10360  axdc3lem4  10375  zornn0g  10427  pwfseqlem4  10585  tskwun  10707  tskint  10708  tskxp  10710  tskmap  10711  gruf  10734  grutsk1  10744  addcanpi  10822  ltapi  10826  mul4  11314  add4  11367  2addsub  11407  addsubeq4  11408  muladd  11582  ltleadd  11633  receu  11795  p1le  12000  mulgt1  12017  lbinf  12109  zdiv  12599  fzind  12627  fnn0ind  12628  fzindd  12631  uzss  12811  zbtwnre  12896  qmulcl  12917  qreccl  12919  xrlttr  13091  xaddass  13201  xmulasslem3  13238  xadddilem  13246  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  iooshf  13379  prunioo  13434  ioojoin  13436  elfz5  13470  elfz0fzfz0  13587  elfzonelfzo  13724  fzind2  13743  modaddb  13868  mulexpz  14064  expsub  14072  digit1  14199  facndiv  14250  faclbnd4lem4  14258  faclbnd4  14259  faclbnd5  14260  bccmpl  14271  bcval5  14280  bcpasc  14283  hashunx  14348  hashunsnggt  14356  hashdmpropge2  14445  ccatrn  14552  swrdspsleq  14628  swrdccat2  14632  ccatpfx  14663  pfxccat1  14664  swrdswrd  14667  cshf1  14772  crim  15077  absmax  15292  ello12r  15479  elo12r  15490  climshftlem  15536  2sumeq2dv  15667  hash2iun  15786  expcnv  15829  2cprodeq2dv  15890  rpnnen2lem7  16187  dvdsval3  16225  dvdsnegb  16242  muldvds1  16249  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  dvdsmulcr  16254  dvds2ln  16258  divalgb  16373  ndvdssub  16378  gcddiv  16520  lcmfval  16590  lcmfcl  16597  dvdslcmf  16600  rpexp1i  16693  phiprmpw  16746  hashgcdeq  16760  pythagtriplem1  16787  pockthg  16877  infpnlem1  16881  4sqlem3  16921  0ramcl  16994  firest  17395  imasaddfnlem  17492  imasleval  17505  mrerintcl  17559  iscatd  17639  fullestrcsetc  18117  fullsetcestrc  18132  clatleglb  18484  mreclatBAD  18529  pslem  18538  mndind  18796  grplmulf1o  18989  grplactcnv  19019  mulgnn0subcl  19063  mulgsubcl  19064  mulgdir  19082  issubg2  19117  issubgrpd2  19118  nmzsubg  19140  eqgen  19156  cycsubm  19177  cycsubgcl  19181  cycsubgss  19182  ghmmulg  19203  ghmf1  19221  kerf1ghm  19222  conjghm  19224  symgpssefmnd  19371  gsmsymgreqlem2  19406  symgfixfo  19414  odeq  19525  odval2  19526  odf1  19537  dfod2  19539  gexdvds  19559  gexdvds2  19560  gexcl2  19564  gexdvds3  19565  sylow2blem2  19596  efgsp1  19712  efgrelexlemb  19725  cmnbascntr  19780  mulgmhm  19802  mulgghm  19803  iscyggen2  19856  iscyg3  19861  ablsimpgfindlem1  20084  ogrpaddltbi  20114  srglmhm  20202  srgrmhm  20203  ringlghm  20293  ringrghm  20294  gsumdixp  20298  dvdsrcl2  20346  crngunit  20358  cntzsubrng  20544  subrgugrp  20568  cntzsubr  20583  rnghmsubcsetclem2  20609  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  sdrgacs  20778  lmodvsdir  20881  lmodvsass  20882  lmodvsghm  20918  lsssubg  20952  lss1d  20958  islbs2  21152  lidlsubg  21221  lidlsubcl  21222  rngqiprngimfo  21299  lpigen  21333  xrsdsreval  21392  expghm  21455  mulgghm2  21456  ip0r  21617  obs2ss  21709  islindf3  21806  scmatscm  22478  scmataddcl  22481  scmatsubcl  22482  scmatfo  22495  matunit  22643  cpmatelimp  22677  cpmatelimp2  22679  cpmatinvcl  22682  cpmatmcl  22684  mat2pmatf  22693  m2cpmf  22707  cpm2mf  22717  m2cpmfo  22721  m2cpminv  22725  decpmataa0  22733  pm2mpf  22763  pm2mpf1  22764  idpm2idmp  22766  pm2mpfo  22779  elcls2  23039  opnnei  23085  innei  23090  iscnp4  23228  cnpnei  23229  iscncl  23234  cnnei  23247  cnconst  23249  ordthauslem  23348  bwth  23375  1stccnp  23427  llyrest  23450  nllyrest  23451  kgenss  23508  xkoccn  23584  kqsat  23696  kqt0lem  23701  isr0  23702  fbssfi  23802  isfild  23823  filconn  23848  trfilss  23854  fgtr  23855  ufileu  23884  ufilen  23895  fmfnfmlem4  23922  fmfnfm  23923  hausflimi  23945  cnpflf2  23965  cnpflf  23966  cnpfcf  24006  cnextcn  24032  tsmsxplem1  24118  tsmsxp  24120  ustuqtop0  24205  ismeti  24290  isxmet2d  24292  elbl2ps  24354  elbl2  24355  xblpnfps  24360  xblpnf  24361  xbln0  24379  blin  24386  blssexps  24391  blssex  24392  blcls  24471  blsscls  24472  metrest  24489  metustbl  24531  psmetutop  24532  nmf2  24558  ngpi  24593  tngngp3  24621  nmdvr  24635  nmoi  24693  nmoix  24694  nmoleub  24696  nghmcn  24710  iccntr  24787  metdsle  24818  icoopnst  24906  iocopnst  24907  icccvx  24917  pi1xfr  25022  isclmi0  25065  iscvsi  25096  cphipval  25210  lmmbr  25225  lmmbr2  25226  iscfil3  25240  iscau2  25244  cfilres  25263  bcthlem1  25291  bcthlem4  25294  bcthlem5  25295  rrxmet  25375  ioombl  25532  iccvolcl  25534  ioovolcl  25537  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  ig1pcl  26144  ig1prsp  26146  aannenlem1  26294  taylplem1  26328  dvtaylp  26335  relogeftb  26548  logdivlt  26585  cxpexp  26632  rpcxpcl  26640  isppw2  27078  vmappw  27079  lgslem4  27263  lgscllem  27267  lgsneg1  27285  lgsne0  27298  nosepdm  27648  sltsdisj  27795  mulcutlem  28123  ltonold  28253  zsoring  28401  bdayfinbndlem1  28459  z12bdaylem  28476  brbtwn2  28974  ax5seglem1  28997  ax5seglem2  28998  axcontlem4  29036  ewlkprop  29672  uspgr2wlkeq  29714  uhgrwkspthlem2  29822  clwlkclwwlkfo  30079  eupth2lem3lem7  30304  frgr3vlem2  30344  3cyclfrgrrn1  30355  4cycl2vnunb  30360  frgrncvvdeqlem8  30376  grpoidinvlem3  30577  isvciOLD  30651  nmcvcn  30766  ipval2lem2  30775  sspimsval  30809  isblo2  30854  nmoo0  30862  blocni  30876  isph  30893  hvadd4  31107  hiassdi  31162  ocsh  31354  chj4  31606  spansncol  31639  pjjsi  31771  hoscl  31816  hodcl  31818  hoadd4  31855  homco1  31872  homulass  31873  hoadddi  31874  hoadddir  31875  unoplin  31991  adjvalval  32008  hmoplin  32013  bralnfn  32019  brafnmul  32022  lnopmi  32071  lnopcoi  32074  hmops  32091  hmopm  32092  nmophmi  32102  lnfncnbd  32128  cnlnadjlem2  32139  adjlnop  32157  adjmul  32163  adjadd  32164  branmfn  32176  kbass5  32191  kbass6  32192  leop2  32195  leopadd  32203  leopmuli  32204  pjimai  32247  atcvatlem  32456  chirredlem2  32462  mdsymlem3  32476  mdsymlem5  32478  sumdmdii  32486  sumdmdlem  32489  cdj3lem2a  32507  cdj3lem2b  32508  cdj3lem3a  32510  cdj3i  32512  nn0difffzod  32877  xreceu  32981  cshwrnid  33021  toslublem  33032  tosglblem  33034  lmodvslmhm  33111  archiabllem1b  33253  archiabllem2c  33256  archiabl  33259  slmdvsdir  33277  slmdvsass  33278  grplsm0l  33463  pidlnzb  33482  rprmndvdsru  33589  mplvrpmmhm  33690  mplvrpmrhm  33691  zarcls1  34013  pstmxmet  34041  ordtconnlem1  34068  hasheuni  34229  omsf  34440  ballotlemirc  34676  signswmnd  34701  bnj1204  35154  fineqvac  35260  fisshasheq  35297  revpfxsfxrev  35298  txpconn  35414  cvmscld  35455  satfbrsuc  35548  satfrnmapom  35552  satfun  35593  elmpps  35755  dfrdg2  35975  wsuclem  36005  segconeu  36193  linecom  36332  linethru  36335  lineintmo  36339  fnemeet2  36549  fnejoin2  36551  fvineqsneq  37728  lindsadd  37934  lindsdom  37935  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  heicant  37976  mblfinlem1  37978  mblfinlem3  37980  ismblfin  37982  cnambfre  37989  itg2addnclem2  37993  ftc1anclem1  38014  ftc1anclem5  38018  ftc1anclem6  38019  ftc2nc  38023  areacirclem2  38030  areacirclem4  38032  areacirclem5  38033  areacirc  38034  fzmul  38062  subspopn  38073  isbndx  38103  isbnd2  38104  isbnd3  38105  ssbnd  38109  prdstotbnd  38115  heibor1  38131  rrnmet  38150  rngonegmn1l  38262  rngohomco  38295  rngoisocnv  38302  rngoisoco  38303  crngohomfo  38327  isidlc  38336  rngoidl  38345  prnc  38388  ispridlc  38391  cvrval2  39720  glbconxN  39824  hlrelat5N  39847  cvratlem  39867  cvrat2  39875  athgt  39902  3dim2  39914  llnn0  39962  lplnn0N  39993  lvoln0N  40037  snatpsubN  40196  paddasslem18  40283  pmod1i  40294  lhpexle2  40456  lhpexle3lem  40457  lhpexle3  40458  ldilcnv  40561  trlcnv  40611  trlnidatb  40623  cdleme32snaw  40881  cdleme32fvaw  40885  cdleme42ke  40931  cdlemeg46gf  40979  cdleme50trn12  40998  cdlemg1cex  41034  cdlemb3  41052  tgrpgrplem  41195  tgrpabl  41197  tendoplcl2  41224  tendo0pl  41237  tendoicl  41242  tendoipl  41243  cdlemkid3N  41379  tendoex  41421  erngdvlem4  41437  erngdvlem4-rN  41445  dib1dim  41611  dib1dim2  41614  dihglbcpreN  41746  dihmeetALTN  41773  dih1dimatlem  41775  dihatlat  41780  lcmineqlem1  42468  lcmineqlem3  42470  aks4d1p1  42515  aks4d1p7d1  42521  aks4d1p8  42526  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones8  42592  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones17  42602  sticksstones19  42604  oddcomabszz  43372  acongtr  43406  rpnnen3lem  43459  islssfg  43498  lmhmfgsplit  43514  unxpwdom3  43523  hbtlem7  43553  iocmbl  43641  ss2iundf  44086  ismnu  44688  grumnudlem  44712  ismnushort  44728  nzss  44744  dvconstbi  44761  bccbc  44772  uzmptshftfval  44773  iccdifprioo  45946  climisp  46174  limsupresxr  46194  liminfresxr  46195  dvnmul  46371  volico  46411  volioore  46418  fourierdlem74  46608  fourierdlem75  46609  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0xp  46857  hspmbllem2  47055  smflimlem3  47201  smfsupmpt  47243  smfinflem  47245  smfinfmpt  47247  smflimsupmpt  47257  smfliminfmpt  47260  funressnbrafv2  47692  uniimaelsetpreimafv  47856  imasetpreimafvbijlemfv1  47863  imasetpreimafvbijlemfo  47865  sprsymrelfo  47957  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  grtrissvtx  48420  gricgrlic  48494  nn0mnd  48655  lcoss  48912  snlindsntorlem  48946  mreclat  49472  aacllem  50276