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  3179  vtocl3  3521  spc3egv  3555  moi2  3672  sbc3ie  3816  2if2  4533  preq12bg  4807  ralxfrd2  5355  reuhypd  5362  otsndisj  5465  funcnvqp  6554  fvtp1g  7142  fntpb  7153  f1imass  7208  weisoeq  7299  f1ofveu  7350  f1ocnvfv3  7351  funeldmdif  7990  curry1f  8046  curry2f  8048  funsssuppss  8130  frrlem13  8238  tfrlem11  8317  oalimcl  8485  oeordsuc  8520  oelim2  8521  nneob  8582  nadd4  8624  mapxpen  9069  findcard  9086  enfii  9108  domtrfil  9114  domnsymfi  9122  phplem2  9127  php  9129  wemaplem3  9451  en2eqpr  9915  infxpabs  10119  infxp  10122  cfflb  10167  cfsmolem  10178  isf32lem12  10272  fin1a2lem9  10316  fin1a2s  10322  axcc3  10346  axdc3lem4  10361  zornn0g  10413  pwfseqlem4  10571  tskwun  10693  tskint  10694  tskxp  10696  tskmap  10697  gruf  10720  grutsk1  10730  addcanpi  10808  ltapi  10812  mul4  11299  add4  11352  2addsub  11392  addsubeq4  11393  muladd  11567  ltleadd  11618  receu  11780  p1le  11984  mulgt1  12001  lbinf  12093  zdiv  12560  fzind  12588  fnn0ind  12589  fzindd  12592  uzss  12772  zbtwnre  12857  qmulcl  12878  qreccl  12880  xrlttr  13052  xaddass  13162  xmulasslem3  13199  xadddilem  13207  xrsupsslem  13220  xrinfmsslem  13221  supxrunb1  13232  ioo0  13284  ico0  13305  ioc0  13306  icc0  13307  iooshf  13340  prunioo  13395  ioojoin  13397  elfz5  13430  elfz0fzfz0  13547  elfzonelfzo  13683  fzind2  13702  modaddb  13827  mulexpz  14023  expsub  14031  digit1  14158  facndiv  14209  faclbnd4lem4  14217  faclbnd4  14218  faclbnd5  14219  bccmpl  14230  bcval5  14239  bcpasc  14242  hashunx  14307  hashunsnggt  14315  hashdmpropge2  14404  ccatrn  14511  swrdspsleq  14587  swrdccat2  14591  ccatpfx  14622  pfxccat1  14623  swrdswrd  14626  cshf1  14731  crim  15036  absmax  15251  ello12r  15438  elo12r  15449  climshftlem  15495  2sumeq2dv  15626  hash2iun  15744  expcnv  15785  2cprodeq2dv  15846  rpnnen2lem7  16143  dvdsval3  16181  dvdsnegb  16198  muldvds1  16205  muldvds2  16206  dvdscmul  16207  dvdsmulc  16208  dvdsmulcr  16210  dvds2ln  16214  divalgb  16329  ndvdssub  16334  gcddiv  16476  lcmfval  16546  lcmfcl  16553  dvdslcmf  16556  rpexp1i  16648  phiprmpw  16701  hashgcdeq  16715  pythagtriplem1  16742  pockthg  16832  infpnlem1  16836  4sqlem3  16876  0ramcl  16949  firest  17350  imasaddfnlem  17447  imasleval  17460  mrerintcl  17514  iscatd  17594  fullestrcsetc  18072  fullsetcestrc  18087  clatleglb  18439  mreclatBAD  18484  pslem  18493  mndind  18751  grplmulf1o  18941  grplactcnv  18971  mulgnn0subcl  19015  mulgsubcl  19016  mulgdir  19034  issubg2  19069  issubgrpd2  19070  nmzsubg  19092  eqgen  19108  cycsubm  19129  cycsubgcl  19133  cycsubgss  19134  ghmmulg  19155  ghmf1  19173  kerf1ghm  19174  conjghm  19176  symgpssefmnd  19323  gsmsymgreqlem2  19358  symgfixfo  19366  odeq  19477  odval2  19478  odf1  19489  dfod2  19491  gexdvds  19511  gexdvds2  19512  gexcl2  19516  gexdvds3  19517  sylow2blem2  19548  efgsp1  19664  efgrelexlemb  19677  cmnbascntr  19732  mulgmhm  19754  mulgghm  19755  iscyggen2  19808  iscyg3  19813  ablsimpgfindlem1  20036  ogrpaddltbi  20066  srglmhm  20154  srgrmhm  20155  ringlghm  20245  ringrghm  20246  gsumdixp  20252  dvdsrcl2  20300  crngunit  20312  cntzsubrng  20498  subrgugrp  20522  cntzsubr  20537  rnghmsubcsetclem2  20563  rhmsubcsetclem2  20592  rhmsubcrngclem2  20598  sdrgacs  20732  lmodvsdir  20835  lmodvsass  20836  lmodvsghm  20872  lsssubg  20906  lss1d  20912  islbs2  21107  lidlsubg  21176  lidlsubcl  21177  rngqiprngimfo  21254  lpigen  21288  xrsdsreval  21364  expghm  21428  mulgghm2  21429  ip0r  21590  obs2ss  21682  islindf3  21779  scmatscm  22455  scmataddcl  22458  scmatsubcl  22459  scmatfo  22472  matunit  22620  cpmatelimp  22654  cpmatelimp2  22656  cpmatinvcl  22659  cpmatmcl  22661  mat2pmatf  22670  m2cpmf  22684  cpm2mf  22694  m2cpmfo  22698  m2cpminv  22702  decpmataa0  22710  pm2mpf  22740  pm2mpf1  22741  idpm2idmp  22743  pm2mpfo  22756  elcls2  23016  opnnei  23062  innei  23067  iscnp4  23205  cnpnei  23206  iscncl  23211  cnnei  23224  cnconst  23226  ordthauslem  23325  bwth  23352  1stccnp  23404  llyrest  23427  nllyrest  23428  kgenss  23485  xkoccn  23561  kqsat  23673  kqt0lem  23678  isr0  23679  fbssfi  23779  isfild  23800  filconn  23825  trfilss  23831  fgtr  23832  ufileu  23861  ufilen  23872  fmfnfmlem4  23899  fmfnfm  23900  hausflimi  23922  cnpflf2  23942  cnpflf  23943  cnpfcf  23983  cnextcn  24009  tsmsxplem1  24095  tsmsxp  24097  ustuqtop0  24182  ismeti  24267  isxmet2d  24269  elbl2ps  24331  elbl2  24332  xblpnfps  24337  xblpnf  24338  xbln0  24356  blin  24363  blssexps  24368  blssex  24369  blcls  24448  blsscls  24449  metrest  24466  metustbl  24508  psmetutop  24509  nmf2  24535  ngpi  24570  tngngp3  24598  nmdvr  24612  nmoi  24670  nmoix  24671  nmoleub  24673  nghmcn  24687  iccntr  24764  metdsle  24795  icoopnst  24890  iocopnst  24891  icccvx  24902  pi1xfr  25009  isclmi0  25052  iscvsi  25083  cphipval  25197  lmmbr  25212  lmmbr2  25213  iscfil3  25227  iscau2  25231  cfilres  25250  bcthlem1  25278  bcthlem4  25281  bcthlem5  25282  rrxmet  25362  ioombl  25520  iccvolcl  25522  ioovolcl  25525  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  ig1pcl  26138  ig1prsp  26140  aannenlem1  26290  taylplem1  26324  dvtaylp  26332  relogeftb  26547  logdivlt  26584  cxpexp  26631  rpcxpcl  26639  isppw2  27079  vmappw  27080  lgslem4  27265  lgscllem  27269  lgsneg1  27287  lgsne0  27300  nosepdm  27650  ssltdisj  27791  mulscutlem  28100  sltonold  28229  zsoring  28367  brbtwn2  28927  ax5seglem1  28950  ax5seglem2  28951  axcontlem4  28989  ewlkprop  29626  uspgr2wlkeq  29668  uhgrwkspthlem2  29776  clwlkclwwlkfo  30033  eupth2lem3lem7  30258  frgr3vlem2  30298  3cyclfrgrrn1  30309  4cycl2vnunb  30314  frgrncvvdeqlem8  30330  grpoidinvlem3  30530  isvciOLD  30604  nmcvcn  30719  ipval2lem2  30728  sspimsval  30762  isblo2  30807  nmoo0  30815  blocni  30829  isph  30846  hvadd4  31060  hiassdi  31115  ocsh  31307  chj4  31559  spansncol  31592  pjjsi  31724  hoscl  31769  hodcl  31771  hoadd4  31808  homco1  31825  homulass  31826  hoadddi  31827  hoadddir  31828  unoplin  31944  adjvalval  31961  hmoplin  31966  bralnfn  31972  brafnmul  31975  lnopmi  32024  lnopcoi  32027  hmops  32044  hmopm  32045  nmophmi  32055  lnfncnbd  32081  cnlnadjlem2  32092  adjlnop  32110  adjmul  32116  adjadd  32117  branmfn  32129  kbass5  32144  kbass6  32145  leop2  32148  leopadd  32156  leopmuli  32157  pjimai  32200  atcvatlem  32409  chirredlem2  32415  mdsymlem3  32429  mdsymlem5  32431  sumdmdii  32439  sumdmdlem  32442  cdj3lem2a  32460  cdj3lem2b  32461  cdj3lem3a  32463  cdj3i  32465  nn0difffzod  32833  xreceu  32952  cshwrnid  32992  toslublem  33003  tosglblem  33005  lmodvslmhm  33082  archiabllem1b  33223  archiabllem2c  33226  archiabl  33229  slmdvsdir  33247  slmdvsass  33248  grplsm0l  33433  pidlnzb  33452  rprmndvdsru  33559  mplvrpmmhm  33660  mplvrpmrhm  33661  zarcls1  33975  pstmxmet  34003  ordtconnlem1  34030  hasheuni  34191  omsf  34402  ballotlemirc  34638  signswmnd  34663  bnj1204  35117  fineqvac  35221  fisshasheq  35258  revpfxsfxrev  35259  txpconn  35375  cvmscld  35416  satfbrsuc  35509  satfrnmapom  35513  satfun  35554  elmpps  35716  dfrdg2  35936  wsuclem  35966  segconeu  36154  linecom  36293  linethru  36296  lineintmo  36300  fnemeet2  36510  fnejoin2  36512  fvineqsneq  37556  lindsadd  37753  lindsdom  37754  lindsenlbs  37755  matunitlindflem1  37756  matunitlindflem2  37757  heicant  37795  mblfinlem1  37797  mblfinlem3  37799  ismblfin  37801  cnambfre  37808  itg2addnclem2  37812  ftc1anclem1  37833  ftc1anclem5  37837  ftc1anclem6  37838  ftc2nc  37842  areacirclem2  37849  areacirclem4  37851  areacirclem5  37852  areacirc  37853  fzmul  37881  subspopn  37892  isbndx  37922  isbnd2  37923  isbnd3  37924  ssbnd  37928  prdstotbnd  37934  heibor1  37950  rrnmet  37969  rngonegmn1l  38081  rngohomco  38114  rngoisocnv  38121  rngoisoco  38122  crngohomfo  38146  isidlc  38155  rngoidl  38164  prnc  38207  ispridlc  38210  cvrval2  39473  glbconxN  39577  hlrelat5N  39600  cvratlem  39620  cvrat2  39628  athgt  39655  3dim2  39667  llnn0  39715  lplnn0N  39746  lvoln0N  39790  snatpsubN  39949  paddasslem18  40036  pmod1i  40047  lhpexle2  40209  lhpexle3lem  40210  lhpexle3  40211  ldilcnv  40314  trlcnv  40364  trlnidatb  40376  cdleme32snaw  40634  cdleme32fvaw  40638  cdleme42ke  40684  cdlemeg46gf  40732  cdleme50trn12  40751  cdlemg1cex  40787  cdlemb3  40805  tgrpgrplem  40948  tgrpabl  40950  tendoplcl2  40977  tendo0pl  40990  tendoicl  40995  tendoipl  40996  cdlemkid3N  41132  tendoex  41174  erngdvlem4  41190  erngdvlem4-rN  41198  dib1dim  41364  dib1dim2  41367  dihglbcpreN  41499  dihmeetALTN  41526  dih1dimatlem  41528  dihatlat  41533  lcmineqlem1  42222  lcmineqlem3  42224  aks4d1p1  42269  aks4d1p7d1  42275  aks4d1p8  42280  sticksstones1  42339  sticksstones2  42340  sticksstones3  42341  sticksstones8  42346  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones12  42351  sticksstones17  42356  sticksstones19  42358  oddcomabszz  43128  acongtr  43162  rpnnen3lem  43215  islssfg  43254  lmhmfgsplit  43270  unxpwdom3  43279  hbtlem7  43309  iocmbl  43397  ss2iundf  43842  ismnu  44444  grumnudlem  44468  ismnushort  44484  nzss  44500  dvconstbi  44517  bccbc  44528  uzmptshftfval  44529  iccdifprioo  45704  climisp  45932  limsupresxr  45952  liminfresxr  45953  dvnmul  46129  volico  46169  volioore  46176  fourierdlem74  46366  fourierdlem75  46367  sge0iunmptlemfi  46599  sge0iunmptlemre  46601  sge0iunmpt  46604  sge0xp  46615  hspmbllem2  46813  smflimlem3  46959  smfsupmpt  47001  smfinflem  47003  smfinfmpt  47005  smflimsupmpt  47015  smfliminfmpt  47018  funressnbrafv2  47432  uniimaelsetpreimafv  47584  imasetpreimafvbijlemfv1  47591  imasetpreimafvbijlemfo  47593  sprsymrelfo  47685  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  grtrissvtx  48132  gricgrlic  48206  nn0mnd  48367  lcoss  48624  snlindsntorlem  48658  mreclat  49184  aacllem  49988