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  3182  vtocl3  3533  spc3egv  3569  moi2  3687  sbc3ie  3831  2if2  4544  preq12bg  4817  ralxfrd2  5367  reuhypd  5374  otsndisj  5479  funcnvqp  6580  fvtp1g  7172  fntpb  7183  f1imass  7239  weisoeq  7330  f1ofveu  7381  f1ocnvfv3  7382  funeldmdif  8027  curry1f  8085  curry2f  8087  funsssuppss  8169  frrlem13  8277  tfrlem11  8356  oalimcl  8524  oeordsuc  8558  oelim2  8559  nneob  8620  nadd4  8662  mapxpen  9107  findcard  9127  enfii  9150  domtrfil  9156  domnsymfi  9164  phplem2  9169  php  9171  wemaplem3  9501  en2eqpr  9960  infxpabs  10164  infxp  10167  cfflb  10212  cfsmolem  10223  isf32lem12  10317  fin1a2lem9  10361  fin1a2s  10367  axcc3  10391  axdc3lem4  10406  zornn0g  10458  pwfseqlem4  10615  tskwun  10737  tskint  10738  tskxp  10740  tskmap  10741  gruf  10764  grutsk1  10774  addcanpi  10852  ltapi  10856  mul4  11342  add4  11395  2addsub  11435  addsubeq4  11436  muladd  11610  ltleadd  11661  receu  11823  p1le  12027  mulgt1  12044  lbinf  12136  zdiv  12604  fzind  12632  fnn0ind  12633  fzindd  12636  uzss  12816  zbtwnre  12905  qmulcl  12926  qreccl  12928  xrlttr  13100  xaddass  13209  xmulasslem3  13246  xadddilem  13254  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  iooshf  13387  prunioo  13442  ioojoin  13444  elfz5  13477  elfz0fzfz0  13594  elfzonelfzo  13730  fzind2  13746  modaddb  13871  mulexpz  14067  expsub  14075  digit1  14202  facndiv  14253  faclbnd4lem4  14261  faclbnd4  14262  faclbnd5  14263  bccmpl  14274  bcval5  14283  bcpasc  14286  hashunx  14351  hashunsnggt  14359  hashdmpropge2  14448  ccatrn  14554  swrdspsleq  14630  swrdccat2  14634  ccatpfx  14666  pfxccat1  14667  swrdswrd  14670  cshf1  14775  crim  15081  absmax  15296  ello12r  15483  elo12r  15494  climshftlem  15540  2sumeq2dv  15671  hash2iun  15789  expcnv  15830  2cprodeq2dv  15891  rpnnen2lem7  16188  dvdsval3  16226  dvdsnegb  16243  muldvds1  16250  muldvds2  16251  dvdscmul  16252  dvdsmulc  16253  dvdsmulcr  16255  dvds2ln  16259  divalgb  16374  ndvdssub  16379  gcddiv  16521  lcmfval  16591  lcmfcl  16598  dvdslcmf  16601  rpexp1i  16693  phiprmpw  16746  hashgcdeq  16760  pythagtriplem1  16787  pockthg  16877  infpnlem1  16881  4sqlem3  16921  0ramcl  16994  firest  17395  imasaddfnlem  17491  imasleval  17504  mrerintcl  17558  iscatd  17634  fullestrcsetc  18112  fullsetcestrc  18127  clatleglb  18477  mreclatBAD  18522  pslem  18531  mndind  18755  grplmulf1o  18945  grplactcnv  18975  mulgnn0subcl  19019  mulgsubcl  19020  mulgdir  19038  issubg2  19073  issubgrpd2  19074  nmzsubg  19097  eqgen  19113  cycsubm  19134  cycsubgcl  19138  cycsubgss  19139  ghmmulg  19160  ghmf1  19178  kerf1ghm  19179  conjghm  19181  symgpssefmnd  19326  gsmsymgreqlem2  19361  symgfixfo  19369  odeq  19480  odval2  19481  odf1  19492  dfod2  19494  gexdvds  19514  gexdvds2  19515  gexcl2  19519  gexdvds3  19520  sylow2blem2  19551  efgsp1  19667  efgrelexlemb  19680  cmnbascntr  19735  mulgmhm  19757  mulgghm  19758  iscyggen2  19811  iscyg3  19816  ablsimpgfindlem1  20039  srglmhm  20130  srgrmhm  20131  ringlghm  20221  ringrghm  20222  gsumdixp  20228  dvdsrcl2  20275  crngunit  20287  cntzsubrng  20476  subrgugrp  20500  cntzsubr  20515  rnghmsubcsetclem2  20541  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  sdrgacs  20710  lmodvsdir  20792  lmodvsass  20793  lmodvsghm  20829  lsssubg  20863  lss1d  20869  islbs2  21064  lidlsubg  21133  lidlsubcl  21134  rngqiprngimfo  21211  lpigen  21245  xrsdsreval  21328  expghm  21385  mulgghm2  21386  ip0r  21546  obs2ss  21638  islindf3  21735  scmatscm  22400  scmataddcl  22403  scmatsubcl  22404  scmatfo  22417  matunit  22565  cpmatelimp  22599  cpmatelimp2  22601  cpmatinvcl  22604  cpmatmcl  22606  mat2pmatf  22615  m2cpmf  22629  cpm2mf  22639  m2cpmfo  22643  m2cpminv  22647  decpmataa0  22655  pm2mpf  22685  pm2mpf1  22686  idpm2idmp  22688  pm2mpfo  22701  elcls2  22961  opnnei  23007  innei  23012  iscnp4  23150  cnpnei  23151  iscncl  23156  cnnei  23169  cnconst  23171  ordthauslem  23270  bwth  23297  1stccnp  23349  llyrest  23372  nllyrest  23373  kgenss  23430  xkoccn  23506  kqsat  23618  kqt0lem  23623  isr0  23624  fbssfi  23724  isfild  23745  filconn  23770  trfilss  23776  fgtr  23777  ufileu  23806  ufilen  23817  fmfnfmlem4  23844  fmfnfm  23845  hausflimi  23867  cnpflf2  23887  cnpflf  23888  cnpfcf  23928  cnextcn  23954  tsmsxplem1  24040  tsmsxp  24042  ustuqtop0  24128  ismeti  24213  isxmet2d  24215  elbl2ps  24277  elbl2  24278  xblpnfps  24283  xblpnf  24284  xbln0  24302  blin  24309  blssexps  24314  blssex  24315  blcls  24394  blsscls  24395  metrest  24412  metustbl  24454  psmetutop  24455  nmf2  24481  ngpi  24516  tngngp3  24544  nmdvr  24558  nmoi  24616  nmoix  24617  nmoleub  24619  nghmcn  24633  iccntr  24710  metdsle  24741  icoopnst  24836  iocopnst  24837  icccvx  24848  pi1xfr  24955  isclmi0  24998  iscvsi  25029  cphipval  25143  lmmbr  25158  lmmbr2  25159  iscfil3  25173  iscau2  25177  cfilres  25196  bcthlem1  25224  bcthlem4  25227  bcthlem5  25228  rrxmet  25308  ioombl  25466  iccvolcl  25468  ioovolcl  25471  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  ig1pcl  26084  ig1prsp  26086  aannenlem1  26236  taylplem1  26270  dvtaylp  26278  relogeftb  26493  logdivlt  26530  cxpexp  26577  rpcxpcl  26585  isppw2  27025  vmappw  27026  lgslem4  27211  lgscllem  27215  lgsneg1  27233  lgsne0  27246  nosepdm  27596  ssltdisj  27733  mulscutlem  28034  sltonold  28162  brbtwn2  28832  ax5seglem1  28855  ax5seglem2  28856  axcontlem4  28894  ewlkprop  29531  uspgr2wlkeq  29574  uhgrwkspthlem2  29684  clwlkclwwlkfo  29938  eupth2lem3lem7  30163  frgr3vlem2  30203  3cyclfrgrrn1  30214  4cycl2vnunb  30219  frgrncvvdeqlem8  30235  grpoidinvlem3  30435  isvciOLD  30509  nmcvcn  30624  ipval2lem2  30633  sspimsval  30667  isblo2  30712  nmoo0  30720  blocni  30734  isph  30751  hvadd4  30965  hiassdi  31020  ocsh  31212  chj4  31464  spansncol  31497  pjjsi  31629  hoscl  31674  hodcl  31676  hoadd4  31713  homco1  31730  homulass  31731  hoadddi  31732  hoadddir  31733  unoplin  31849  adjvalval  31866  hmoplin  31871  bralnfn  31877  brafnmul  31880  lnopmi  31929  lnopcoi  31932  hmops  31949  hmopm  31950  nmophmi  31960  lnfncnbd  31986  cnlnadjlem2  31997  adjlnop  32015  adjmul  32021  adjadd  32022  branmfn  32034  kbass5  32049  kbass6  32050  leop2  32053  leopadd  32061  leopmuli  32062  pjimai  32105  atcvatlem  32314  chirredlem2  32320  mdsymlem3  32334  mdsymlem5  32336  sumdmdii  32344  sumdmdlem  32347  cdj3lem2a  32365  cdj3lem2b  32366  cdj3lem3a  32368  cdj3i  32370  nn0difffzod  32729  xreceu  32842  cshwrnid  32883  toslublem  32898  tosglblem  32900  lmodvslmhm  32990  ogrpaddltbi  33032  archiabllem1b  33146  archiabllem2c  33149  archiabl  33152  slmdvsdir  33169  slmdvsass  33170  grplsm0l  33374  pidlnzb  33393  rprmndvdsru  33500  zarcls1  33859  pstmxmet  33887  ordtconnlem1  33914  hasheuni  34075  omsf  34287  ballotlemirc  34523  signswmnd  34548  bnj1204  35002  fineqvac  35087  fisshasheq  35102  revpfxsfxrev  35103  txpconn  35219  cvmscld  35260  satfbrsuc  35353  satfrnmapom  35357  satfun  35398  elmpps  35560  dfrdg2  35783  wsuclem  35813  segconeu  35999  linecom  36138  linethru  36141  lineintmo  36145  fnemeet2  36355  fnejoin2  36357  fvineqsneq  37400  lindsadd  37607  lindsdom  37608  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  heicant  37649  mblfinlem1  37651  mblfinlem3  37653  ismblfin  37655  cnambfre  37662  itg2addnclem2  37666  ftc1anclem1  37687  ftc1anclem5  37691  ftc1anclem6  37692  ftc2nc  37696  areacirclem2  37703  areacirclem4  37705  areacirclem5  37706  areacirc  37707  fzmul  37735  subspopn  37746  isbndx  37776  isbnd2  37777  isbnd3  37778  ssbnd  37782  prdstotbnd  37788  heibor1  37804  rrnmet  37823  rngonegmn1l  37935  rngohomco  37968  rngoisocnv  37975  rngoisoco  37976  crngohomfo  38000  isidlc  38009  rngoidl  38018  prnc  38061  ispridlc  38064  cvrval2  39267  glbconxN  39372  hlrelat5N  39395  cvratlem  39415  cvrat2  39423  athgt  39450  3dim2  39462  llnn0  39510  lplnn0N  39541  lvoln0N  39585  snatpsubN  39744  paddasslem18  39831  pmod1i  39842  lhpexle2  40004  lhpexle3lem  40005  lhpexle3  40006  ldilcnv  40109  trlcnv  40159  trlnidatb  40171  cdleme32snaw  40429  cdleme32fvaw  40433  cdleme42ke  40479  cdlemeg46gf  40527  cdleme50trn12  40546  cdlemg1cex  40582  cdlemb3  40600  tgrpgrplem  40743  tgrpabl  40745  tendoplcl2  40772  tendo0pl  40785  tendoicl  40790  tendoipl  40791  cdlemkid3N  40927  tendoex  40969  erngdvlem4  40985  erngdvlem4-rN  40993  dib1dim  41159  dib1dim2  41162  dihglbcpreN  41294  dihmeetALTN  41321  dih1dimatlem  41323  dihatlat  41328  lcmineqlem1  42017  lcmineqlem3  42019  aks4d1p1  42064  aks4d1p7d1  42070  aks4d1p8  42075  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones8  42141  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones17  42151  sticksstones19  42153  oddcomabszz  42933  acongtr  42967  rpnnen3lem  43020  islssfg  43059  lmhmfgsplit  43075  unxpwdom3  43084  hbtlem7  43114  iocmbl  43202  ss2iundf  43648  ismnu  44250  grumnudlem  44274  ismnushort  44290  nzss  44306  dvconstbi  44323  bccbc  44334  uzmptshftfval  44335  iccdifprioo  45514  climisp  45744  limsupresxr  45764  liminfresxr  45765  dvnmul  45941  volico  45981  volioore  45988  fourierdlem74  46178  fourierdlem75  46179  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0xp  46427  hspmbllem2  46625  smflimlem3  46771  smfsupmpt  46813  smfinflem  46815  smfinfmpt  46817  smflimsupmpt  46827  smfliminfmpt  46830  funressnbrafv2  47245  uniimaelsetpreimafv  47397  imasetpreimafvbijlemfv1  47404  imasetpreimafvbijlemfo  47406  sprsymrelfo  47498  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  grtrissvtx  47943  gricgrlic  48010  nn0mnd  48167  lcoss  48425  snlindsntorlem  48459  mreclat  48985  aacllem  49790