Theorem 3expa 1136

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-3an 1105

This theorem is used by:  3exp  1137  ad4ant123  1191  ad4ant124  1192  ad4ant134  1193  ad4ant234  1194  ad5ant123  1387  ad5ant124  1388  ad5ant125  1390  3anidm23  1448  mp3an2  1478  mpd3an3  1491  rgen3  3207  vtocl3  3527  spc3egv  3557  moi2  3674  sbc3ie  3816  2if2  4538  preq12bg  4813  ralxfrd2  5377  reuhypd  5384  otsndisj  5496  funcnvqp  6598  fvtp1g  7197  fntpb  7209  f1imass  7262  weisoeq  7359  f1ofveu  7408  f1ocnvfv3  7409  funeldmdif  8046  curry1f  8104  curry2f  8106  funsssuppss  8189  frrlem13  8298  tfrlem11  8378  oalimcl  8550  oeordsuc  8585  oelim2  8586  nneob  8647  nadd4  8690  mapxpen  9144  findcard  9161  enfii  9183  domtrfil  9189  domnsymfi  9197  phplem2  9202  php  9204  wemaplem3  9523  en2eqpr  10013  infxpabs  10216  infxp  10219  cfflb  10264  cfsmolem  10275  isf32lem12  10369  fin1a2lem9  10413  fin1a2s  10419  axcc3  10443  axdc3lem4  10458  zornn0g  10510  pwfseqlem4  10674  tskwun  10796  tskint  10797  tskxp  10799  tskmap  10800  gruf  10823  grutsk1  10833  addcanpi  10911  ltapi  10915  mul4  11405  add4  11458  2addsub  11498  addsubeq4  11499  muladd  11673  ltleadd  11724  receu  11886  p1le  12087  mulgt1  12103  lbinf  12195  zdiv  12694  fzind  12722  fnn0ind  12723  fzindd  12726  uzss  12913  zbtwnre  12998  qmulcl  13020  qreccl  13022  xrlttr  13194  xaddass  13304  xmulasslem3  13341  xadddilem  13349  xrsupsslem  13362  xrinfmsslem  13363  supxrunb1  13374  ioo0  13426  ico0  13447  ioc0  13448  icc0  13449  iooshf  13482  prunioo  13537  ioojoin  13539  elfz5  13573  elfz0fzfz0  13691  elfzonelfzo  13828  fzind2  13847  modaddb  13973  mulexpz  14169  expsub  14177  digit1  14304  facndiv  14355  faclbnd4lem4  14363  faclbnd4  14364  faclbnd5  14365  bccmpl  14376  bcval5  14385  bcpasc  14388  hashunx  14453  hashunsnggt  14461  hashdmpropge2  14551  ccatrn  14658  swrdspsleq  14738  swrdccat2  14742  ccatpfx  14773  pfxccat1  14774  swrdswrd  14777  revpfxsfxrev  14840  cshf1  14884  crim  15205  absmax  15420  ello12r  15607  elo12r  15618  climshftlem  15664  2sumeq2dv  15794  hash2iun  15913  expcnv  15956  2cprodeq2dv  16015  rpnnen2lem7  16311  dvdsval3  16349  dvdsnegb  16366  muldvds1  16373  muldvds2  16374  dvdscmul  16375  dvdsmulc  16376  dvdsmulcr  16378  dvds2ln  16382  divalgb  16497  ndvdssub  16502  gcddiv  16644  lcmfval  16714  lcmfcl  16721  dvdslcmf  16724  rpexp1i  16817  phiprmpw  16870  hashgcdeq  16884  pythagtriplem1  16911  pockthg  17001  infpnlem1  17005  4sqlem3  17045  0ramcl  17118  firest  17520  imasaddfnlem  17617  imasleval  17630  mrerintcl  17684  iscatd  17764  fullestrcsetc  18242  fullsetcestrc  18257  clatleglb  18609  mreclatBAD  18654  pslem  18663  mndind  18940  grplmulf1o  19139  grplactcnv  19169  mulgnn0subcl  19213  mulgsubcl  19214  mulgdir  19232  issubg2  19268  issubgrpd2  19269  nmzsubg  19291  eqgen  19309  cycsubm  19333  cycsubgcl  19337  cycsubgss  19338  ghmmulg  19358  ghmf1  19376  kerf1ghm  19377  conjghm  19379  symgpssefmnd  19526  gsmsymgreqlem2  19561  symgfixfo  19569  odeq  19680  odval2  19681  odf1  19692  dfod2  19694  gexdvds  19714  gexdvds2  19715  gexcl2  19719  gexdvds3  19720  sylow2blem2  19751  efgsp1  19867  efgrelexlemb  19880  cmnbascntr  19935  mulgmhm  19957  mulgghm  19958  iscyggen2  20011  iscyg3  20016  ablsimpgfindlem1  20239  ogrpaddltbi  20269  srglmhm  20363  srgrmhm  20364  ringlghm  20457  ringrghm  20458  gsumdixp  20462  dvdsrcl2  20510  crngunit  20522  cntzsubrng  20732  subrgugrp  20756  cntzsubr  20771  rnghmsubcsetclem2  20797  rhmsubcsetclem2  20826  rhmsubcrngclem2  20832  sdrgacs  20970  lmodvsdir  21073  lmodvsass  21074  lmodvsghm  21110  lsssubg  21144  lss1d  21150  islbs2  21344  lidlsubg  21414  lidlsubcl  21415  rngqiprngimfo  21507  lpigen  21569  xrsdsreval  21628  expghm  21691  mulgghm2  21692  ip0r  21853  obs2ss  21945  islindf3  22042  lindsdom  22066  lindsenlbs  22067  scmatscm  22738  scmataddcl  22741  scmatsubcl  22742  scmatfo  22755  matunit  22903  matunitlindflem1  22904  matunitlindflem2  22905  cpmatelimp  22940  cpmatelimp2  22942  cpmatinvcl  22945  cpmatmcl  22947  mat2pmatf  22956  m2cpmf  22970  cpm2mf  22980  m2cpmfo  22984  m2cpminv  22988  decpmataa0  22996  pm2mpf  23026  pm2mpf1  23027  idpm2idmp  23029  pm2mpfo  23042  elcls2  23302  opnnei  23348  innei  23353  iscnp4  23491  cnpnei  23492  iscncl  23497  cnnei  23510  cnconst  23512  ordthauslem  23611  bwth  23638  1stccnp  23691  llyrest  23714  nllyrest  23715  kgenss  23772  xkoccn  23848  kqsat  23960  kqt0lem  23965  isr0  23966  fbssfi  24066  isfild  24087  filconn  24112  trfilss  24118  fgtr  24119  ufileu  24148  ufilen  24159  fmfnfmlem4  24186  fmfnfm  24187  hausflimi  24209  cnpflf2  24229  cnpflf  24230  cnpfcf  24270  cnextcn  24296  tsmsxplem1  24382  tsmsxp  24384  ustuqtop0  24469  ismeti  24554  isxmet2d  24556  elbl2ps  24618  elbl2  24619  xblpnfps  24624  xblpnf  24625  xbln0  24643  blin  24650  blssexps  24655  blssex  24656  blcls  24735  blsscls  24736  metrest  24753  metustbl  24795  psmetutop  24796  nmf2  24822  ngpi  24857  tngngp3  24885  nmdvr  24899  nmoi  24957  nmoix  24958  nmoleub  24960  nghmcn  24974  iccntr  25051  metdsle  25082  icoopnst  25170  iocopnst  25171  icccvx  25181  pi1xfr  25286  isclmi0  25329  iscvsi  25360  cphipval  25474  lmmbr  25489  lmmbr2  25490  iscfil3  25504  iscau2  25508  cfilres  25527  bcthlem1  25555  bcthlem4  25558  bcthlem5  25559  rrxmet  25639  ioombl  25796  iccvolcl  25798  ioovolcl  25801  mbfi1fseqlem3  25948  mbfi1fseqlem4  25949  mbfi1fseqlem5  25950  ig1pcl  26407  ig1prsp  26409  aannenlem1  26567  taylplem1  26602  dvtaylp  26609  relogeftb  26824  logdivlt  26861  cxpexp  26908  rpcxpcl  26916  isppw2  27354  vmappw  27355  lgslem4  27539  lgscllem  27543  lgsneg1  27561  lgsne0  27574  nosepdm  27923  sltsdisj  28071  mulcutlem  28399  ltonold  28529  zsoring  28677  bdayfinbndlem1  28735  z12bdaylem  28752  brbtwn2  29365  ax5seglem1  29388  ax5seglem2  29389  axcontlem4  29427  ewlkprop  30066  uspgr2wlkeq  30108  uhgrwkspthlem2  30222  clwlkclwwlkfo  30482  eupth2lem3lem7  30717  frgr3vlem2  30757  3cyclfrgrrn1  30768  4cycl2vnunb  30773  frgrncvvdeqlem8  30789  grpoidinvlem3  30990  isvciOLD  31064  nmcvcn  31179  ipval2lem2  31188  sspimsval  31222  isblo2  31267  nmoo0  31275  blocni  31289  isph  31306  hvadd4  31520  hiassdi  31575  ocsh  31767  chj4  32019  spansncol  32052  pjjsi  32184  hoscl  32229  hodcl  32231  hoadd4  32268  homco1  32285  homulass  32286  hoadddi  32287  hoadddir  32288  unoplin  32404  adjvalval  32421  hmoplin  32426  bralnfn  32432  brafnmul  32435  lnopmi  32484  lnopcoi  32487  hmops  32504  hmopm  32505  nmophmi  32515  lnfncnbd  32541  cnlnadjlem2  32552  adjlnop  32570  adjmul  32576  adjadd  32577  branmfn  32589  kbass5  32604  kbass6  32605  leop2  32608  leopadd  32616  leopmuli  32617  pjimai  32660  atcvatlem  32869  chirredlem2  32875  mdsymlem3  32889  mdsymlem5  32891  sumdmdii  32899  sumdmdlem  32902  cdj3lem2a  32920  cdj3lem2b  32921  cdj3lem3a  32923  cdj3i  32925  nn0difffzod  33278  xreceu  33370  cshwrnid  33404  toslublem  33415  tosglblem  33417  lmodvslmhm  33493  archiabllem1b  33635  archiabllem2c  33638  archiabl  33641  slmdvsdir  33659  slmdvsass  33660  grplsm0l  33835  pidlnzb  33853  rprmndvdsru  33942  mplvrpmmhm  34059  mplvrpmrhm  34060  zarcls1  34382  pstmxmet  34410  ordtconnlem1  34437  hasheuni  34598  omsf  34810  ballotlemirc  35046  signswmnd  35068  bnj1204  35524  fineqvac  35645  fisshasheq  35720  txpconn  35814  cvmscld  35855  satfbrsuc  35948  satfrnmapom  35952  satfun  35993  elmpps  36155  dfrdg2  36375  wsuclem  36405  segconeu  36594  linecom  36733  linethru  36736  lineintmo  36740  fnemeet2  36989  fnejoin2  36991  fvineqsneq  38169  lindsadd  38370  heicant  38407  mblfinlem1  38409  mblfinlem3  38411  ismblfin  38413  cnambfre  38420  itg2addnclem2  38424  ftc1anclem1  38445  ftc1anclem5  38449  ftc1anclem6  38450  ftc2nc  38454  areacirclem2  38461  areacirclem4  38463  areacirclem5  38464  areacirc  38465  fzmul  38494  subspopn  38505  isbndx  38535  isbnd2  38536  isbnd3  38537  ssbnd  38541  prdstotbnd  38547  heibor1  38563  rrnmet  38582  rngonegmn1l  38694  rngohomco  38727  rngoisocnv  38734  rngoisoco  38735  crngohomfo  38759  isidlc  38768  rngoidl  38777  prnc  38820  ispridlc  38823  cvrval2  40150  glbconxN  40254  hlrelat5N  40277  cvratlem  40297  cvrat2  40305  athgt  40332  3dim2  40344  llnn0  40392  lplnn0N  40423  lvoln0N  40467  snatpsubN  40626  paddasslem18  40713  pmod1i  40724  lhpexle2  40886  lhpexle3lem  40887  lhpexle3  40888  ldilcnv  40991  trlcnv  41041  trlnidatb  41053  cdleme32snaw  41311  cdleme32fvaw  41315  cdleme42ke  41361  cdlemeg46gf  41409  cdleme50trn12  41428  cdlemg1cex  41464  cdlemb3  41482  tgrpgrplem  41625  tgrpabl  41627  tendoplcl2  41654  tendo0pl  41667  tendoicl  41672  tendoipl  41673  cdlemkid3N  41809  tendoex  41851  erngdvlem4  41867  erngdvlem4-rN  41875  dib1dim  42041  dib1dim2  42044  dihglbcpreN  42176  dihmeetALTN  42203  dih1dimatlem  42205  dihatlat  42210  lcmineqlem1  42898  lcmineqlem3  42900  aks4d1p1  42945  aks4d1p7d1  42951  aks4d1p8  42956  sticksstones1  43015  sticksstones2  43016  sticksstones3  43017  sticksstones8  43022  sticksstones10  43024  sticksstones11  43025  sticksstones12a  43026  sticksstones12  43027  sticksstones17  43032  sticksstones19  43034  oddcomabszz  43788  acongtr  43822  rpnnen3lem  43875  islssfg  43914  lmhmfgsplit  43930  unxpwdom3  43939  hbtlem7  43969  iocmbl  44057  ss2iundf  44502  ismnu  45088  grumnudlem  45112  ismnushort  45128  nzss  45144  dvconstbi  45161  bccbc  45172  uzmptshftfval  45173  iccdifprioo  46349  climisp  46577  limsupresxr  46597  liminfresxr  46598  dvnmul  46774  volico  46814  volioore  46821  fourierdlem74  47011  fourierdlem75  47012  sge0iunmptlemfi  47244  sge0iunmptlemre  47246  sge0iunmpt  47249  sge0xp  47260  hspmbllem2  47458  smflimlem3  47604  smfsupmpt  47646  smfinflem  47648  smfinfmpt  47650  smflimsupmpt  47660  smfliminfmpt  47663  funressnbrafv2  48135  uniimaelsetpreimafv  48299  imasetpreimafvbijlemfv1  48306  imasetpreimafvbijlemfo  48308  sprsymrelfo  48400  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  grtrissvtx  48863  gricgrlic  48937  nn0mnd  49097  lcoss  49369  snlindsntorlem  49403  mreclat  49926  aacllem  50775