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  3183  vtocl3  3525  spc3egv  3559  moi2  3676  sbc3ie  3820  2if2  4537  preq12bg  4811  ralxfrd2  5359  reuhypd  5366  otsndisj  5475  funcnvqp  6564  fvtp1g  7154  fntpb  7165  f1imass  7220  weisoeq  7311  f1ofveu  7362  f1ocnvfv3  7363  funeldmdif  8002  curry1f  8058  curry2f  8060  funsssuppss  8142  frrlem13  8250  tfrlem11  8329  oalimcl  8497  oeordsuc  8532  oelim2  8533  nneob  8594  nadd4  8636  mapxpen  9083  findcard  9100  enfii  9122  domtrfil  9128  domnsymfi  9136  phplem2  9141  php  9143  wemaplem3  9465  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  11313  add4  11366  2addsub  11406  addsubeq4  11407  muladd  11581  ltleadd  11632  receu  11794  p1le  11998  mulgt1  12015  lbinf  12107  zdiv  12574  fzind  12602  fnn0ind  12603  fzindd  12606  uzss  12786  zbtwnre  12871  qmulcl  12892  qreccl  12894  xrlttr  13066  xaddass  13176  xmulasslem3  13213  xadddilem  13221  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  iooshf  13354  prunioo  13409  ioojoin  13411  elfz5  13444  elfz0fzfz0  13561  elfzonelfzo  13697  fzind2  13716  modaddb  13841  mulexpz  14037  expsub  14045  digit1  14172  facndiv  14223  faclbnd4lem4  14231  faclbnd4  14232  faclbnd5  14233  bccmpl  14244  bcval5  14253  bcpasc  14256  hashunx  14321  hashunsnggt  14329  hashdmpropge2  14418  ccatrn  14525  swrdspsleq  14601  swrdccat2  14605  ccatpfx  14636  pfxccat1  14637  swrdswrd  14640  cshf1  14745  crim  15050  absmax  15265  ello12r  15452  elo12r  15463  climshftlem  15509  2sumeq2dv  15640  hash2iun  15758  expcnv  15799  2cprodeq2dv  15860  rpnnen2lem7  16157  dvdsval3  16195  dvdsnegb  16212  muldvds1  16219  muldvds2  16220  dvdscmul  16221  dvdsmulc  16222  dvdsmulcr  16224  dvds2ln  16228  divalgb  16343  ndvdssub  16348  gcddiv  16490  lcmfval  16560  lcmfcl  16567  dvdslcmf  16570  rpexp1i  16662  phiprmpw  16715  hashgcdeq  16729  pythagtriplem1  16756  pockthg  16846  infpnlem1  16850  4sqlem3  16890  0ramcl  16963  firest  17364  imasaddfnlem  17461  imasleval  17474  mrerintcl  17528  iscatd  17608  fullestrcsetc  18086  fullsetcestrc  18101  clatleglb  18453  mreclatBAD  18498  pslem  18507  mndind  18765  grplmulf1o  18958  grplactcnv  18988  mulgnn0subcl  19032  mulgsubcl  19033  mulgdir  19051  issubg2  19086  issubgrpd2  19087  nmzsubg  19109  eqgen  19125  cycsubm  19146  cycsubgcl  19150  cycsubgss  19151  ghmmulg  19172  ghmf1  19190  kerf1ghm  19191  conjghm  19193  symgpssefmnd  19340  gsmsymgreqlem2  19375  symgfixfo  19383  odeq  19494  odval2  19495  odf1  19506  dfod2  19508  gexdvds  19528  gexdvds2  19529  gexcl2  19533  gexdvds3  19534  sylow2blem2  19565  efgsp1  19681  efgrelexlemb  19694  cmnbascntr  19749  mulgmhm  19771  mulgghm  19772  iscyggen2  19825  iscyg3  19830  ablsimpgfindlem1  20053  ogrpaddltbi  20083  srglmhm  20171  srgrmhm  20172  ringlghm  20262  ringrghm  20263  gsumdixp  20269  dvdsrcl2  20317  crngunit  20329  cntzsubrng  20515  subrgugrp  20539  cntzsubr  20554  rnghmsubcsetclem2  20580  rhmsubcsetclem2  20609  rhmsubcrngclem2  20615  sdrgacs  20749  lmodvsdir  20852  lmodvsass  20853  lmodvsghm  20889  lsssubg  20923  lss1d  20929  islbs2  21124  lidlsubg  21193  lidlsubcl  21194  rngqiprngimfo  21271  lpigen  21305  xrsdsreval  21381  expghm  21445  mulgghm2  21446  ip0r  21607  obs2ss  21699  islindf3  21796  scmatscm  22472  scmataddcl  22475  scmatsubcl  22476  scmatfo  22489  matunit  22637  cpmatelimp  22671  cpmatelimp2  22673  cpmatinvcl  22676  cpmatmcl  22678  mat2pmatf  22687  m2cpmf  22701  cpm2mf  22711  m2cpmfo  22715  m2cpminv  22719  decpmataa0  22727  pm2mpf  22757  pm2mpf1  22758  idpm2idmp  22760  pm2mpfo  22773  elcls2  23033  opnnei  23079  innei  23084  iscnp4  23222  cnpnei  23223  iscncl  23228  cnnei  23241  cnconst  23243  ordthauslem  23342  bwth  23369  1stccnp  23421  llyrest  23444  nllyrest  23445  kgenss  23502  xkoccn  23578  kqsat  23690  kqt0lem  23695  isr0  23696  fbssfi  23796  isfild  23817  filconn  23842  trfilss  23848  fgtr  23849  ufileu  23878  ufilen  23889  fmfnfmlem4  23916  fmfnfm  23917  hausflimi  23939  cnpflf2  23959  cnpflf  23960  cnpfcf  24000  cnextcn  24026  tsmsxplem1  24112  tsmsxp  24114  ustuqtop0  24199  ismeti  24284  isxmet2d  24286  elbl2ps  24348  elbl2  24349  xblpnfps  24354  xblpnf  24355  xbln0  24373  blin  24380  blssexps  24385  blssex  24386  blcls  24465  blsscls  24466  metrest  24483  metustbl  24525  psmetutop  24526  nmf2  24552  ngpi  24587  tngngp3  24615  nmdvr  24629  nmoi  24687  nmoix  24688  nmoleub  24690  nghmcn  24704  iccntr  24781  metdsle  24812  icoopnst  24907  iocopnst  24908  icccvx  24919  pi1xfr  25026  isclmi0  25069  iscvsi  25100  cphipval  25214  lmmbr  25229  lmmbr2  25230  iscfil3  25244  iscau2  25248  cfilres  25267  bcthlem1  25295  bcthlem4  25298  bcthlem5  25299  rrxmet  25379  ioombl  25537  iccvolcl  25539  ioovolcl  25542  mbfi1fseqlem3  25689  mbfi1fseqlem4  25690  mbfi1fseqlem5  25691  ig1pcl  26155  ig1prsp  26157  aannenlem1  26307  taylplem1  26341  dvtaylp  26349  relogeftb  26564  logdivlt  26601  cxpexp  26648  rpcxpcl  26656  isppw2  27096  vmappw  27097  lgslem4  27282  lgscllem  27286  lgsneg1  27304  lgsne0  27317  nosepdm  27667  sltsdisj  27814  mulcutlem  28142  ltonold  28272  zsoring  28420  bdayfinbndlem1  28478  z12bdaylem  28495  brbtwn2  28994  ax5seglem1  29017  ax5seglem2  29018  axcontlem4  29056  ewlkprop  29693  uspgr2wlkeq  29735  uhgrwkspthlem2  29843  clwlkclwwlkfo  30100  eupth2lem3lem7  30325  frgr3vlem2  30365  3cyclfrgrrn1  30376  4cycl2vnunb  30381  frgrncvvdeqlem8  30397  grpoidinvlem3  30598  isvciOLD  30672  nmcvcn  30787  ipval2lem2  30796  sspimsval  30830  isblo2  30875  nmoo0  30883  blocni  30897  isph  30914  hvadd4  31128  hiassdi  31183  ocsh  31375  chj4  31627  spansncol  31660  pjjsi  31792  hoscl  31837  hodcl  31839  hoadd4  31876  homco1  31893  homulass  31894  hoadddi  31895  hoadddir  31896  unoplin  32012  adjvalval  32029  hmoplin  32034  bralnfn  32040  brafnmul  32043  lnopmi  32092  lnopcoi  32095  hmops  32112  hmopm  32113  nmophmi  32123  lnfncnbd  32149  cnlnadjlem2  32160  adjlnop  32178  adjmul  32184  adjadd  32185  branmfn  32197  kbass5  32212  kbass6  32213  leop2  32216  leopadd  32224  leopmuli  32225  pjimai  32268  atcvatlem  32477  chirredlem2  32483  mdsymlem3  32497  mdsymlem5  32499  sumdmdii  32507  sumdmdlem  32510  cdj3lem2a  32528  cdj3lem2b  32529  cdj3lem3a  32531  cdj3i  32533  nn0difffzod  32899  xreceu  33018  cshwrnid  33058  toslublem  33069  tosglblem  33071  lmodvslmhm  33148  archiabllem1b  33290  archiabllem2c  33293  archiabl  33296  slmdvsdir  33314  slmdvsass  33315  grplsm0l  33500  pidlnzb  33519  rprmndvdsru  33626  mplvrpmmhm  33727  mplvrpmrhm  33728  zarcls1  34051  pstmxmet  34079  ordtconnlem1  34106  hasheuni  34267  omsf  34478  ballotlemirc  34714  signswmnd  34739  bnj1204  35192  fineqvac  35298  fisshasheq  35335  revpfxsfxrev  35336  txpconn  35452  cvmscld  35493  satfbrsuc  35586  satfrnmapom  35590  satfun  35631  elmpps  35793  dfrdg2  36013  wsuclem  36043  segconeu  36231  linecom  36370  linethru  36373  lineintmo  36377  fnemeet2  36587  fnejoin2  36589  fvineqsneq  37671  lindsadd  37868  lindsdom  37869  lindsenlbs  37870  matunitlindflem1  37871  matunitlindflem2  37872  heicant  37910  mblfinlem1  37912  mblfinlem3  37914  ismblfin  37916  cnambfre  37923  itg2addnclem2  37927  ftc1anclem1  37948  ftc1anclem5  37952  ftc1anclem6  37953  ftc2nc  37957  areacirclem2  37964  areacirclem4  37966  areacirclem5  37967  areacirc  37968  fzmul  37996  subspopn  38007  isbndx  38037  isbnd2  38038  isbnd3  38039  ssbnd  38043  prdstotbnd  38049  heibor1  38065  rrnmet  38084  rngonegmn1l  38196  rngohomco  38229  rngoisocnv  38236  rngoisoco  38237  crngohomfo  38261  isidlc  38270  rngoidl  38279  prnc  38322  ispridlc  38325  cvrval2  39654  glbconxN  39758  hlrelat5N  39781  cvratlem  39801  cvrat2  39809  athgt  39836  3dim2  39848  llnn0  39896  lplnn0N  39927  lvoln0N  39971  snatpsubN  40130  paddasslem18  40217  pmod1i  40228  lhpexle2  40390  lhpexle3lem  40391  lhpexle3  40392  ldilcnv  40495  trlcnv  40545  trlnidatb  40557  cdleme32snaw  40815  cdleme32fvaw  40819  cdleme42ke  40865  cdlemeg46gf  40913  cdleme50trn12  40932  cdlemg1cex  40968  cdlemb3  40986  tgrpgrplem  41129  tgrpabl  41131  tendoplcl2  41158  tendo0pl  41171  tendoicl  41176  tendoipl  41177  cdlemkid3N  41313  tendoex  41355  erngdvlem4  41371  erngdvlem4-rN  41379  dib1dim  41545  dib1dim2  41548  dihglbcpreN  41680  dihmeetALTN  41707  dih1dimatlem  41709  dihatlat  41714  lcmineqlem1  42403  lcmineqlem3  42405  aks4d1p1  42450  aks4d1p7d1  42456  aks4d1p8  42461  sticksstones1  42520  sticksstones2  42521  sticksstones3  42522  sticksstones8  42527  sticksstones10  42529  sticksstones11  42530  sticksstones12a  42531  sticksstones12  42532  sticksstones17  42537  sticksstones19  42539  oddcomabszz  43305  acongtr  43339  rpnnen3lem  43392  islssfg  43431  lmhmfgsplit  43447  unxpwdom3  43456  hbtlem7  43486  iocmbl  43574  ss2iundf  44019  ismnu  44621  grumnudlem  44645  ismnushort  44661  nzss  44677  dvconstbi  44694  bccbc  44705  uzmptshftfval  44706  iccdifprioo  45880  climisp  46108  limsupresxr  46128  liminfresxr  46129  dvnmul  46305  volico  46345  volioore  46352  fourierdlem74  46542  fourierdlem75  46543  sge0iunmptlemfi  46775  sge0iunmptlemre  46777  sge0iunmpt  46780  sge0xp  46791  hspmbllem2  46989  smflimlem3  47135  smfsupmpt  47177  smfinflem  47179  smfinfmpt  47181  smflimsupmpt  47191  smfliminfmpt  47194  funressnbrafv2  47608  uniimaelsetpreimafv  47760  imasetpreimafvbijlemfv1  47767  imasetpreimafvbijlemfo  47769  sprsymrelfo  47861  nnsum4primesodd  48160  nnsum4primesoddALTV  48161  grtrissvtx  48308  gricgrlic  48382  nn0mnd  48543  lcoss  48800  snlindsntorlem  48834  mreclat  49360  aacllem  50164