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  3213  vtocl3  3535  spc3egv  3565  moi2  3682  sbc3ie  3824  2if2  4548  preq12bg  4823  ralxfrd2  5388  reuhypd  5395  otsndisj  5507  funcnvqp  6607  fvtp1g  7203  fntpb  7214  f1imass  7269  weisoeq  7366  f1ofveu  7417  f1ocnvfv3  7418  funeldmdif  8054  curry1f  8110  curry2f  8112  funsssuppss  8195  frrlem13  8304  tfrlem11  8384  oalimcl  8554  oeordsuc  8589  oelim2  8590  nneob  8651  nadd4  8694  mapxpen  9141  findcard  9158  enfii  9180  domtrfil  9186  domnsymfi  9194  phplem2  9199  php  9201  wemaplem3  9520  en2eqpr  10010  infxpabs  10213  infxp  10216  cfflb  10261  cfsmolem  10272  isf32lem12  10366  fin1a2lem9  10410  fin1a2s  10416  axcc3  10440  axdc3lem4  10455  zornn0g  10507  pwfseqlem4  10665  tskwun  10787  tskint  10788  tskxp  10790  tskmap  10791  gruf  10814  grutsk1  10824  addcanpi  10902  ltapi  10906  mul4  11396  add4  11449  2addsub  11489  addsubeq4  11490  muladd  11664  ltleadd  11715  receu  11877  p1le  12078  mulgt1  12094  lbinf  12186  zdiv  12684  fzind  12712  fnn0ind  12713  fzindd  12716  uzss  12903  zbtwnre  12988  qmulcl  13009  qreccl  13011  xrlttr  13183  xaddass  13293  xmulasslem3  13330  xadddilem  13338  xrsupsslem  13351  xrinfmsslem  13352  supxrunb1  13363  ioo0  13415  ico0  13436  ioc0  13437  icc0  13438  iooshf  13471  prunioo  13526  ioojoin  13528  elfz5  13562  elfz0fzfz0  13680  elfzonelfzo  13817  fzind2  13836  modaddb  13962  mulexpz  14158  expsub  14166  digit1  14293  facndiv  14344  faclbnd4lem4  14352  faclbnd4  14353  faclbnd5  14354  bccmpl  14365  bcval5  14374  bcpasc  14377  hashunx  14442  hashunsnggt  14450  hashdmpropge2  14540  ccatrn  14647  swrdspsleq  14727  swrdccat2  14731  ccatpfx  14762  pfxccat1  14763  swrdswrd  14766  revpfxsfxrev  14829  cshf1  14873  crim  15192  absmax  15407  ello12r  15594  elo12r  15605  climshftlem  15651  2sumeq2dv  15782  hash2iun  15901  expcnv  15944  2cprodeq2dv  16005  rpnnen2lem7  16301  dvdsval3  16339  dvdsnegb  16356  muldvds1  16363  muldvds2  16364  dvdscmul  16365  dvdsmulc  16366  dvdsmulcr  16368  dvds2ln  16372  divalgb  16487  ndvdssub  16492  gcddiv  16634  lcmfval  16704  lcmfcl  16711  dvdslcmf  16714  rpexp1i  16807  phiprmpw  16860  hashgcdeq  16874  pythagtriplem1  16901  pockthg  16991  infpnlem1  16995  4sqlem3  17035  0ramcl  17108  firest  17510  imasaddfnlem  17607  imasleval  17620  mrerintcl  17674  iscatd  17754  fullestrcsetc  18232  fullsetcestrc  18247  clatleglb  18599  mreclatBAD  18644  pslem  18653  mndind  18912  grplmulf1o  19104  grplactcnv  19134  mulgnn0subcl  19178  mulgsubcl  19179  mulgdir  19197  issubg2  19233  issubgrpd2  19234  nmzsubg  19256  eqgen  19274  cycsubm  19298  cycsubgcl  19302  cycsubgss  19303  ghmmulg  19323  ghmf1  19341  kerf1ghm  19342  conjghm  19344  symgpssefmnd  19491  gsmsymgreqlem2  19526  symgfixfo  19534  odeq  19645  odval2  19646  odf1  19657  dfod2  19659  gexdvds  19679  gexdvds2  19680  gexcl2  19684  gexdvds3  19685  sylow2blem2  19716  efgsp1  19832  efgrelexlemb  19845  cmnbascntr  19900  mulgmhm  19922  mulgghm  19923  iscyggen2  19976  iscyg3  19981  ablsimpgfindlem1  20204  ogrpaddltbi  20234  srglmhm  20328  srgrmhm  20329  ringlghm  20421  ringrghm  20422  gsumdixp  20426  dvdsrcl2  20474  crngunit  20486  cntzsubrng  20696  subrgugrp  20720  cntzsubr  20735  rnghmsubcsetclem2  20761  rhmsubcsetclem2  20790  rhmsubcrngclem2  20796  sdrgacs  20934  lmodvsdir  21037  lmodvsass  21038  lmodvsghm  21074  lsssubg  21108  lss1d  21114  islbs2  21308  lidlsubg  21378  lidlsubcl  21379  rngqiprngimfo  21471  lpigen  21533  xrsdsreval  21592  expghm  21655  mulgghm2  21656  ip0r  21817  obs2ss  21909  islindf3  22006  scmatscm  22700  scmataddcl  22703  scmatsubcl  22704  scmatfo  22717  matunit  22865  cpmatelimp  22899  cpmatelimp2  22901  cpmatinvcl  22904  cpmatmcl  22906  mat2pmatf  22915  m2cpmf  22929  cpm2mf  22939  m2cpmfo  22943  m2cpminv  22947  decpmataa0  22955  pm2mpf  22985  pm2mpf1  22986  idpm2idmp  22988  pm2mpfo  23001  elcls2  23261  opnnei  23307  innei  23312  iscnp4  23450  cnpnei  23451  iscncl  23456  cnnei  23469  cnconst  23471  ordthauslem  23570  bwth  23597  1stccnp  23649  llyrest  23672  nllyrest  23673  kgenss  23730  xkoccn  23806  kqsat  23918  kqt0lem  23923  isr0  23924  fbssfi  24024  isfild  24045  filconn  24070  trfilss  24076  fgtr  24077  ufileu  24106  ufilen  24117  fmfnfmlem4  24144  fmfnfm  24145  hausflimi  24167  cnpflf2  24187  cnpflf  24188  cnpfcf  24228  cnextcn  24254  tsmsxplem1  24340  tsmsxp  24342  ustuqtop0  24427  ismeti  24512  isxmet2d  24514  elbl2ps  24576  elbl2  24577  xblpnfps  24582  xblpnf  24583  xbln0  24601  blin  24608  blssexps  24613  blssex  24614  blcls  24693  blsscls  24694  metrest  24711  metustbl  24753  psmetutop  24754  nmf2  24780  ngpi  24815  tngngp3  24843  nmdvr  24857  nmoi  24915  nmoix  24916  nmoleub  24918  nghmcn  24932  iccntr  25009  metdsle  25040  icoopnst  25128  iocopnst  25129  icccvx  25139  pi1xfr  25244  isclmi0  25287  iscvsi  25318  cphipval  25432  lmmbr  25447  lmmbr2  25448  iscfil3  25462  iscau2  25466  cfilres  25485  bcthlem1  25513  bcthlem4  25516  bcthlem5  25517  rrxmet  25597  ioombl  25754  iccvolcl  25756  ioovolcl  25759  mbfi1fseqlem3  25906  mbfi1fseqlem4  25907  mbfi1fseqlem5  25908  ig1pcl  26366  ig1prsp  26368  aannenlem1  26521  taylplem1  26556  dvtaylp  26563  relogeftb  26779  logdivlt  26816  cxpexp  26863  rpcxpcl  26871  isppw2  27309  vmappw  27310  lgslem4  27494  lgscllem  27498  lgsneg1  27516  lgsne0  27529  nosepdm  27878  sltsdisj  28026  mulcutlem  28354  ltonold  28484  zsoring  28632  bdayfinbndlem1  28690  z12bdaylem  28707  brbtwn2  29285  ax5seglem1  29308  ax5seglem2  29309  axcontlem4  29347  ewlkprop  29983  uspgr2wlkeq  30025  uhgrwkspthlem2  30133  clwlkclwwlkfo  30390  eupth2lem3lem7  30615  frgr3vlem2  30655  3cyclfrgrrn1  30666  4cycl2vnunb  30671  frgrncvvdeqlem8  30687  grpoidinvlem3  30888  isvciOLD  30962  nmcvcn  31077  ipval2lem2  31086  sspimsval  31120  isblo2  31165  nmoo0  31173  blocni  31187  isph  31204  hvadd4  31418  hiassdi  31473  ocsh  31665  chj4  31917  spansncol  31950  pjjsi  32082  hoscl  32127  hodcl  32129  hoadd4  32166  homco1  32183  homulass  32184  hoadddi  32185  hoadddir  32186  unoplin  32302  adjvalval  32319  hmoplin  32324  bralnfn  32330  brafnmul  32333  lnopmi  32382  lnopcoi  32385  hmops  32402  hmopm  32403  nmophmi  32413  lnfncnbd  32439  cnlnadjlem2  32450  adjlnop  32468  adjmul  32474  adjadd  32475  branmfn  32487  kbass5  32502  kbass6  32503  leop2  32506  leopadd  32514  leopmuli  32515  pjimai  32558  atcvatlem  32767  chirredlem2  32773  mdsymlem3  32787  mdsymlem5  32789  sumdmdii  32797  sumdmdlem  32800  cdj3lem2a  32818  cdj3lem2b  32819  cdj3lem3a  32821  cdj3i  32823  nn0difffzod  33179  xreceu  33271  cshwrnid  33305  toslublem  33316  tosglblem  33318  lmodvslmhm  33394  archiabllem1b  33536  archiabllem2c  33539  archiabl  33542  slmdvsdir  33560  slmdvsass  33561  grplsm0l  33736  pidlnzb  33754  rprmndvdsru  33843  mplvrpmmhm  33960  mplvrpmrhm  33961  zarcls1  34283  pstmxmet  34311  ordtconnlem1  34338  hasheuni  34499  omsf  34710  ballotlemirc  34946  signswmnd  34968  bnj1204  35424  fineqvac  35545  fisshasheq  35621  txpconn  35737  cvmscld  35778  satfbrsuc  35871  satfrnmapom  35875  satfun  35916  elmpps  36078  dfrdg2  36298  wsuclem  36328  segconeu  36516  linecom  36655  linethru  36658  lineintmo  36662  fnemeet2  36911  fnejoin2  36913  fvineqsneq  38091  lindsadd  38297  lindsdom  38298  lindsenlbs  38299  matunitlindflem1  38300  matunitlindflem2  38301  heicant  38339  mblfinlem1  38341  mblfinlem3  38343  ismblfin  38345  cnambfre  38352  itg2addnclem2  38356  ftc1anclem1  38377  ftc1anclem5  38381  ftc1anclem6  38382  ftc2nc  38386  areacirclem2  38393  areacirclem4  38395  areacirclem5  38396  areacirc  38397  fzmul  38425  subspopn  38436  isbndx  38466  isbnd2  38467  isbnd3  38468  ssbnd  38472  prdstotbnd  38478  heibor1  38494  rrnmet  38513  rngonegmn1l  38625  rngohomco  38658  rngoisocnv  38665  rngoisoco  38666  crngohomfo  38690  isidlc  38699  rngoidl  38708  prnc  38751  ispridlc  38754  cvrval2  40081  glbconxN  40185  hlrelat5N  40208  cvratlem  40228  cvrat2  40236  athgt  40263  3dim2  40275  llnn0  40323  lplnn0N  40354  lvoln0N  40398  snatpsubN  40557  paddasslem18  40644  pmod1i  40655  lhpexle2  40817  lhpexle3lem  40818  lhpexle3  40819  ldilcnv  40922  trlcnv  40972  trlnidatb  40984  cdleme32snaw  41242  cdleme32fvaw  41246  cdleme42ke  41292  cdlemeg46gf  41340  cdleme50trn12  41359  cdlemg1cex  41395  cdlemb3  41413  tgrpgrplem  41556  tgrpabl  41558  tendoplcl2  41585  tendo0pl  41598  tendoicl  41603  tendoipl  41604  cdlemkid3N  41740  tendoex  41782  erngdvlem4  41798  erngdvlem4-rN  41806  dib1dim  41972  dib1dim2  41975  dihglbcpreN  42107  dihmeetALTN  42134  dih1dimatlem  42136  dihatlat  42141  lcmineqlem1  42829  lcmineqlem3  42831  aks4d1p1  42876  aks4d1p7d1  42882  aks4d1p8  42887  sticksstones1  42946  sticksstones2  42947  sticksstones3  42948  sticksstones8  42953  sticksstones10  42955  sticksstones11  42956  sticksstones12a  42957  sticksstones12  42958  sticksstones17  42963  sticksstones19  42965  oddcomabszz  43704  acongtr  43738  rpnnen3lem  43791  islssfg  43830  lmhmfgsplit  43846  unxpwdom3  43855  hbtlem7  43885  iocmbl  43973  ss2iundf  44418  ismnu  45004  grumnudlem  45028  ismnushort  45044  nzss  45060  dvconstbi  45077  bccbc  45088  uzmptshftfval  45089  iccdifprioo  46265  climisp  46493  limsupresxr  46513  liminfresxr  46514  dvnmul  46690  volico  46730  volioore  46737  fourierdlem74  46927  fourierdlem75  46928  sge0iunmptlemfi  47160  sge0iunmptlemre  47162  sge0iunmpt  47165  sge0xp  47176  hspmbllem2  47374  smflimlem3  47520  smfsupmpt  47562  smfinflem  47564  smfinfmpt  47566  smflimsupmpt  47576  smfliminfmpt  47579  funressnbrafv2  48014  uniimaelsetpreimafv  48178  imasetpreimafvbijlemfv1  48185  imasetpreimafvbijlemfo  48187  sprsymrelfo  48279  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  grtrissvtx  48742  gricgrlic  48816  nn0mnd  48977  lcoss  49249  snlindsntorlem  49283  mreclat  49808  aacllem  50654