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  3177  vtocl3  3519  spc3egv  3553  moi2  3670  sbc3ie  3814  2if2  4528  preq12bg  4802  ralxfrd2  5348  reuhypd  5355  otsndisj  5457  funcnvqp  6545  fvtp1g  7132  fntpb  7143  f1imass  7198  weisoeq  7289  f1ofveu  7340  f1ocnvfv3  7341  funeldmdif  7980  curry1f  8036  curry2f  8038  funsssuppss  8120  frrlem13  8228  tfrlem11  8307  oalimcl  8475  oeordsuc  8509  oelim2  8510  nneob  8571  nadd4  8613  mapxpen  9056  findcard  9073  enfii  9095  domtrfil  9101  domnsymfi  9109  phplem2  9114  php  9116  wemaplem3  9434  en2eqpr  9898  infxpabs  10102  infxp  10105  cfflb  10150  cfsmolem  10161  isf32lem12  10255  fin1a2lem9  10299  fin1a2s  10305  axcc3  10329  axdc3lem4  10344  zornn0g  10396  pwfseqlem4  10553  tskwun  10675  tskint  10676  tskxp  10678  tskmap  10679  gruf  10702  grutsk1  10712  addcanpi  10790  ltapi  10794  mul4  11281  add4  11334  2addsub  11374  addsubeq4  11375  muladd  11549  ltleadd  11600  receu  11762  p1le  11966  mulgt1  11983  lbinf  12075  zdiv  12543  fzind  12571  fnn0ind  12572  fzindd  12575  uzss  12755  zbtwnre  12844  qmulcl  12865  qreccl  12867  xrlttr  13039  xaddass  13148  xmulasslem3  13185  xadddilem  13193  xrsupsslem  13206  xrinfmsslem  13207  supxrunb1  13218  ioo0  13270  ico0  13291  ioc0  13292  icc0  13293  iooshf  13326  prunioo  13381  ioojoin  13383  elfz5  13416  elfz0fzfz0  13533  elfzonelfzo  13669  fzind2  13688  modaddb  13813  mulexpz  14009  expsub  14017  digit1  14144  facndiv  14195  faclbnd4lem4  14203  faclbnd4  14204  faclbnd5  14205  bccmpl  14216  bcval5  14225  bcpasc  14228  hashunx  14293  hashunsnggt  14301  hashdmpropge2  14390  ccatrn  14497  swrdspsleq  14573  swrdccat2  14577  ccatpfx  14608  pfxccat1  14609  swrdswrd  14612  cshf1  14717  crim  15022  absmax  15237  ello12r  15424  elo12r  15435  climshftlem  15481  2sumeq2dv  15612  hash2iun  15730  expcnv  15771  2cprodeq2dv  15832  rpnnen2lem7  16129  dvdsval3  16167  dvdsnegb  16184  muldvds1  16191  muldvds2  16192  dvdscmul  16193  dvdsmulc  16194  dvdsmulcr  16196  dvds2ln  16200  divalgb  16315  ndvdssub  16320  gcddiv  16462  lcmfval  16532  lcmfcl  16539  dvdslcmf  16542  rpexp1i  16634  phiprmpw  16687  hashgcdeq  16701  pythagtriplem1  16728  pockthg  16818  infpnlem1  16822  4sqlem3  16862  0ramcl  16935  firest  17336  imasaddfnlem  17432  imasleval  17445  mrerintcl  17499  iscatd  17579  fullestrcsetc  18057  fullsetcestrc  18072  clatleglb  18424  mreclatBAD  18469  pslem  18478  mndind  18736  grplmulf1o  18926  grplactcnv  18956  mulgnn0subcl  19000  mulgsubcl  19001  mulgdir  19019  issubg2  19054  issubgrpd2  19055  nmzsubg  19077  eqgen  19093  cycsubm  19114  cycsubgcl  19118  cycsubgss  19119  ghmmulg  19140  ghmf1  19158  kerf1ghm  19159  conjghm  19161  symgpssefmnd  19308  gsmsymgreqlem2  19343  symgfixfo  19351  odeq  19462  odval2  19463  odf1  19474  dfod2  19476  gexdvds  19496  gexdvds2  19497  gexcl2  19501  gexdvds3  19502  sylow2blem2  19533  efgsp1  19649  efgrelexlemb  19662  cmnbascntr  19717  mulgmhm  19739  mulgghm  19740  iscyggen2  19793  iscyg3  19798  ablsimpgfindlem1  20021  ogrpaddltbi  20051  srglmhm  20139  srgrmhm  20140  ringlghm  20230  ringrghm  20231  gsumdixp  20237  dvdsrcl2  20284  crngunit  20296  cntzsubrng  20482  subrgugrp  20506  cntzsubr  20521  rnghmsubcsetclem2  20547  rhmsubcsetclem2  20576  rhmsubcrngclem2  20582  sdrgacs  20716  lmodvsdir  20819  lmodvsass  20820  lmodvsghm  20856  lsssubg  20890  lss1d  20896  islbs2  21091  lidlsubg  21160  lidlsubcl  21161  rngqiprngimfo  21238  lpigen  21272  xrsdsreval  21348  expghm  21412  mulgghm2  21413  ip0r  21574  obs2ss  21666  islindf3  21763  scmatscm  22428  scmataddcl  22431  scmatsubcl  22432  scmatfo  22445  matunit  22593  cpmatelimp  22627  cpmatelimp2  22629  cpmatinvcl  22632  cpmatmcl  22634  mat2pmatf  22643  m2cpmf  22657  cpm2mf  22667  m2cpmfo  22671  m2cpminv  22675  decpmataa0  22683  pm2mpf  22713  pm2mpf1  22714  idpm2idmp  22716  pm2mpfo  22729  elcls2  22989  opnnei  23035  innei  23040  iscnp4  23178  cnpnei  23179  iscncl  23184  cnnei  23197  cnconst  23199  ordthauslem  23298  bwth  23325  1stccnp  23377  llyrest  23400  nllyrest  23401  kgenss  23458  xkoccn  23534  kqsat  23646  kqt0lem  23651  isr0  23652  fbssfi  23752  isfild  23773  filconn  23798  trfilss  23804  fgtr  23805  ufileu  23834  ufilen  23845  fmfnfmlem4  23872  fmfnfm  23873  hausflimi  23895  cnpflf2  23915  cnpflf  23916  cnpfcf  23956  cnextcn  23982  tsmsxplem1  24068  tsmsxp  24070  ustuqtop0  24155  ismeti  24240  isxmet2d  24242  elbl2ps  24304  elbl2  24305  xblpnfps  24310  xblpnf  24311  xbln0  24329  blin  24336  blssexps  24341  blssex  24342  blcls  24421  blsscls  24422  metrest  24439  metustbl  24481  psmetutop  24482  nmf2  24508  ngpi  24543  tngngp3  24571  nmdvr  24585  nmoi  24643  nmoix  24644  nmoleub  24646  nghmcn  24660  iccntr  24737  metdsle  24768  icoopnst  24863  iocopnst  24864  icccvx  24875  pi1xfr  24982  isclmi0  25025  iscvsi  25056  cphipval  25170  lmmbr  25185  lmmbr2  25186  iscfil3  25200  iscau2  25204  cfilres  25223  bcthlem1  25251  bcthlem4  25254  bcthlem5  25255  rrxmet  25335  ioombl  25493  iccvolcl  25495  ioovolcl  25498  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  ig1pcl  26111  ig1prsp  26113  aannenlem1  26263  taylplem1  26297  dvtaylp  26305  relogeftb  26520  logdivlt  26557  cxpexp  26604  rpcxpcl  26612  isppw2  27052  vmappw  27053  lgslem4  27238  lgscllem  27242  lgsneg1  27260  lgsne0  27273  nosepdm  27623  ssltdisj  27764  mulscutlem  28070  sltonold  28198  zsoring  28332  brbtwn2  28883  ax5seglem1  28906  ax5seglem2  28907  axcontlem4  28945  ewlkprop  29582  uspgr2wlkeq  29624  uhgrwkspthlem2  29732  clwlkclwwlkfo  29989  eupth2lem3lem7  30214  frgr3vlem2  30254  3cyclfrgrrn1  30265  4cycl2vnunb  30270  frgrncvvdeqlem8  30286  grpoidinvlem3  30486  isvciOLD  30560  nmcvcn  30675  ipval2lem2  30684  sspimsval  30718  isblo2  30763  nmoo0  30771  blocni  30785  isph  30802  hvadd4  31016  hiassdi  31071  ocsh  31263  chj4  31515  spansncol  31548  pjjsi  31680  hoscl  31725  hodcl  31727  hoadd4  31764  homco1  31781  homulass  31782  hoadddi  31783  hoadddir  31784  unoplin  31900  adjvalval  31917  hmoplin  31922  bralnfn  31928  brafnmul  31931  lnopmi  31980  lnopcoi  31983  hmops  32000  hmopm  32001  nmophmi  32011  lnfncnbd  32037  cnlnadjlem2  32048  adjlnop  32066  adjmul  32072  adjadd  32073  branmfn  32085  kbass5  32100  kbass6  32101  leop2  32104  leopadd  32112  leopmuli  32113  pjimai  32156  atcvatlem  32365  chirredlem2  32371  mdsymlem3  32385  mdsymlem5  32387  sumdmdii  32395  sumdmdlem  32398  cdj3lem2a  32416  cdj3lem2b  32417  cdj3lem3a  32419  cdj3i  32421  nn0difffzod  32786  xreceu  32902  cshwrnid  32942  toslublem  32953  tosglblem  32955  lmodvslmhm  33030  archiabllem1b  33161  archiabllem2c  33164  archiabl  33167  slmdvsdir  33185  slmdvsass  33186  grplsm0l  33368  pidlnzb  33387  rprmndvdsru  33494  mplvrpmmhm  33576  mplvrpmrhm  33577  zarcls1  33882  pstmxmet  33910  ordtconnlem1  33937  hasheuni  34098  omsf  34309  ballotlemirc  34545  signswmnd  34570  bnj1204  35024  fineqvac  35139  fisshasheq  35159  revpfxsfxrev  35160  txpconn  35276  cvmscld  35317  satfbrsuc  35410  satfrnmapom  35414  satfun  35455  elmpps  35617  dfrdg2  35837  wsuclem  35867  segconeu  36055  linecom  36194  linethru  36197  lineintmo  36201  fnemeet2  36411  fnejoin2  36413  fvineqsneq  37456  lindsadd  37663  lindsdom  37664  lindsenlbs  37665  matunitlindflem1  37666  matunitlindflem2  37667  heicant  37705  mblfinlem1  37707  mblfinlem3  37709  ismblfin  37711  cnambfre  37718  itg2addnclem2  37722  ftc1anclem1  37743  ftc1anclem5  37747  ftc1anclem6  37748  ftc2nc  37752  areacirclem2  37759  areacirclem4  37761  areacirclem5  37762  areacirc  37763  fzmul  37791  subspopn  37802  isbndx  37832  isbnd2  37833  isbnd3  37834  ssbnd  37838  prdstotbnd  37844  heibor1  37860  rrnmet  37879  rngonegmn1l  37991  rngohomco  38024  rngoisocnv  38031  rngoisoco  38032  crngohomfo  38056  isidlc  38065  rngoidl  38074  prnc  38117  ispridlc  38120  cvrval2  39383  glbconxN  39487  hlrelat5N  39510  cvratlem  39530  cvrat2  39538  athgt  39565  3dim2  39577  llnn0  39625  lplnn0N  39656  lvoln0N  39700  snatpsubN  39859  paddasslem18  39946  pmod1i  39957  lhpexle2  40119  lhpexle3lem  40120  lhpexle3  40121  ldilcnv  40224  trlcnv  40274  trlnidatb  40286  cdleme32snaw  40544  cdleme32fvaw  40548  cdleme42ke  40594  cdlemeg46gf  40642  cdleme50trn12  40661  cdlemg1cex  40697  cdlemb3  40715  tgrpgrplem  40858  tgrpabl  40860  tendoplcl2  40887  tendo0pl  40900  tendoicl  40905  tendoipl  40906  cdlemkid3N  41042  tendoex  41084  erngdvlem4  41100  erngdvlem4-rN  41108  dib1dim  41274  dib1dim2  41277  dihglbcpreN  41409  dihmeetALTN  41436  dih1dimatlem  41438  dihatlat  41443  lcmineqlem1  42132  lcmineqlem3  42134  aks4d1p1  42179  aks4d1p7d1  42185  aks4d1p8  42190  sticksstones1  42249  sticksstones2  42250  sticksstones3  42251  sticksstones8  42256  sticksstones10  42258  sticksstones11  42259  sticksstones12a  42260  sticksstones12  42261  sticksstones17  42266  sticksstones19  42268  oddcomabszz  43047  acongtr  43081  rpnnen3lem  43134  islssfg  43173  lmhmfgsplit  43189  unxpwdom3  43198  hbtlem7  43228  iocmbl  43316  ss2iundf  43762  ismnu  44364  grumnudlem  44388  ismnushort  44404  nzss  44420  dvconstbi  44437  bccbc  44448  uzmptshftfval  44449  iccdifprioo  45626  climisp  45854  limsupresxr  45874  liminfresxr  45875  dvnmul  46051  volico  46091  volioore  46098  fourierdlem74  46288  fourierdlem75  46289  sge0iunmptlemfi  46521  sge0iunmptlemre  46523  sge0iunmpt  46526  sge0xp  46537  hspmbllem2  46735  smflimlem3  46881  smfsupmpt  46923  smfinflem  46925  smfinfmpt  46927  smflimsupmpt  46937  smfliminfmpt  46940  funressnbrafv2  47354  uniimaelsetpreimafv  47506  imasetpreimafvbijlemfv1  47513  imasetpreimafvbijlemfo  47515  sprsymrelfo  47607  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  grtrissvtx  48054  gricgrlic  48128  nn0mnd  48289  lcoss  48547  snlindsntorlem  48581  mreclat  49107  aacllem  49912