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  3180  vtocl3  3530  spc3egv  3566  moi2  3684  sbc3ie  3828  2if2  4540  preq12bg  4813  ralxfrd2  5362  reuhypd  5369  otsndisj  5474  funcnvqp  6564  fvtp1g  7154  fntpb  7165  f1imass  7221  weisoeq  7312  f1ofveu  7363  f1ocnvfv3  7364  funeldmdif  8006  curry1f  8062  curry2f  8064  funsssuppss  8146  frrlem13  8254  tfrlem11  8333  oalimcl  8501  oeordsuc  8535  oelim2  8536  nneob  8597  nadd4  8639  mapxpen  9084  findcard  9104  enfii  9127  domtrfil  9133  domnsymfi  9141  phplem2  9146  php  9148  wemaplem3  9477  en2eqpr  9936  infxpabs  10140  infxp  10143  cfflb  10188  cfsmolem  10199  isf32lem12  10293  fin1a2lem9  10337  fin1a2s  10343  axcc3  10367  axdc3lem4  10382  zornn0g  10434  pwfseqlem4  10591  tskwun  10713  tskint  10714  tskxp  10716  tskmap  10717  gruf  10740  grutsk1  10750  addcanpi  10828  ltapi  10832  mul4  11318  add4  11371  2addsub  11411  addsubeq4  11412  muladd  11586  ltleadd  11637  receu  11799  p1le  12003  mulgt1  12020  lbinf  12112  zdiv  12580  fzind  12608  fnn0ind  12609  fzindd  12612  uzss  12792  zbtwnre  12881  qmulcl  12902  qreccl  12904  xrlttr  13076  xaddass  13185  xmulasslem3  13222  xadddilem  13230  xrsupsslem  13243  xrinfmsslem  13244  supxrunb1  13255  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  iooshf  13363  prunioo  13418  ioojoin  13420  elfz5  13453  elfz0fzfz0  13570  elfzonelfzo  13706  fzind2  13722  modaddb  13847  mulexpz  14043  expsub  14051  digit1  14178  facndiv  14229  faclbnd4lem4  14237  faclbnd4  14238  faclbnd5  14239  bccmpl  14250  bcval5  14259  bcpasc  14262  hashunx  14327  hashunsnggt  14335  hashdmpropge2  14424  ccatrn  14530  swrdspsleq  14606  swrdccat2  14610  ccatpfx  14642  pfxccat1  14643  swrdswrd  14646  cshf1  14751  crim  15057  absmax  15272  ello12r  15459  elo12r  15470  climshftlem  15516  2sumeq2dv  15647  hash2iun  15765  expcnv  15806  2cprodeq2dv  15867  rpnnen2lem7  16164  dvdsval3  16202  dvdsnegb  16219  muldvds1  16226  muldvds2  16227  dvdscmul  16228  dvdsmulc  16229  dvdsmulcr  16231  dvds2ln  16235  divalgb  16350  ndvdssub  16355  gcddiv  16497  lcmfval  16567  lcmfcl  16574  dvdslcmf  16577  rpexp1i  16669  phiprmpw  16722  hashgcdeq  16736  pythagtriplem1  16763  pockthg  16853  infpnlem1  16857  4sqlem3  16897  0ramcl  16970  firest  17371  imasaddfnlem  17467  imasleval  17480  mrerintcl  17534  iscatd  17614  fullestrcsetc  18092  fullsetcestrc  18107  clatleglb  18459  mreclatBAD  18504  pslem  18513  mndind  18737  grplmulf1o  18927  grplactcnv  18957  mulgnn0subcl  19001  mulgsubcl  19002  mulgdir  19020  issubg2  19055  issubgrpd2  19056  nmzsubg  19079  eqgen  19095  cycsubm  19116  cycsubgcl  19120  cycsubgss  19121  ghmmulg  19142  ghmf1  19160  kerf1ghm  19161  conjghm  19163  symgpssefmnd  19310  gsmsymgreqlem2  19345  symgfixfo  19353  odeq  19464  odval2  19465  odf1  19476  dfod2  19478  gexdvds  19498  gexdvds2  19499  gexcl2  19503  gexdvds3  19504  sylow2blem2  19535  efgsp1  19651  efgrelexlemb  19664  cmnbascntr  19719  mulgmhm  19741  mulgghm  19742  iscyggen2  19795  iscyg3  19800  ablsimpgfindlem1  20023  ogrpaddltbi  20053  srglmhm  20141  srgrmhm  20142  ringlghm  20232  ringrghm  20233  gsumdixp  20239  dvdsrcl2  20286  crngunit  20298  cntzsubrng  20487  subrgugrp  20511  cntzsubr  20526  rnghmsubcsetclem2  20552  rhmsubcsetclem2  20581  rhmsubcrngclem2  20587  sdrgacs  20721  lmodvsdir  20824  lmodvsass  20825  lmodvsghm  20861  lsssubg  20895  lss1d  20901  islbs2  21096  lidlsubg  21165  lidlsubcl  21166  rngqiprngimfo  21243  lpigen  21277  xrsdsreval  21353  expghm  21417  mulgghm2  21418  ip0r  21579  obs2ss  21671  islindf3  21768  scmatscm  22433  scmataddcl  22436  scmatsubcl  22437  scmatfo  22450  matunit  22598  cpmatelimp  22632  cpmatelimp2  22634  cpmatinvcl  22637  cpmatmcl  22639  mat2pmatf  22648  m2cpmf  22662  cpm2mf  22672  m2cpmfo  22676  m2cpminv  22680  decpmataa0  22688  pm2mpf  22718  pm2mpf1  22719  idpm2idmp  22721  pm2mpfo  22734  elcls2  22994  opnnei  23040  innei  23045  iscnp4  23183  cnpnei  23184  iscncl  23189  cnnei  23202  cnconst  23204  ordthauslem  23303  bwth  23330  1stccnp  23382  llyrest  23405  nllyrest  23406  kgenss  23463  xkoccn  23539  kqsat  23651  kqt0lem  23656  isr0  23657  fbssfi  23757  isfild  23778  filconn  23803  trfilss  23809  fgtr  23810  ufileu  23839  ufilen  23850  fmfnfmlem4  23877  fmfnfm  23878  hausflimi  23900  cnpflf2  23920  cnpflf  23921  cnpfcf  23961  cnextcn  23987  tsmsxplem1  24073  tsmsxp  24075  ustuqtop0  24161  ismeti  24246  isxmet2d  24248  elbl2ps  24310  elbl2  24311  xblpnfps  24316  xblpnf  24317  xbln0  24335  blin  24342  blssexps  24347  blssex  24348  blcls  24427  blsscls  24428  metrest  24445  metustbl  24487  psmetutop  24488  nmf2  24514  ngpi  24549  tngngp3  24577  nmdvr  24591  nmoi  24649  nmoix  24650  nmoleub  24652  nghmcn  24666  iccntr  24743  metdsle  24774  icoopnst  24869  iocopnst  24870  icccvx  24881  pi1xfr  24988  isclmi0  25031  iscvsi  25062  cphipval  25176  lmmbr  25191  lmmbr2  25192  iscfil3  25206  iscau2  25210  cfilres  25229  bcthlem1  25257  bcthlem4  25260  bcthlem5  25261  rrxmet  25341  ioombl  25499  iccvolcl  25501  ioovolcl  25504  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  ig1pcl  26117  ig1prsp  26119  aannenlem1  26269  taylplem1  26303  dvtaylp  26311  relogeftb  26526  logdivlt  26563  cxpexp  26610  rpcxpcl  26618  isppw2  27058  vmappw  27059  lgslem4  27244  lgscllem  27248  lgsneg1  27266  lgsne0  27279  nosepdm  27629  ssltdisj  27769  mulscutlem  28074  sltonold  28202  zsoring  28336  brbtwn2  28885  ax5seglem1  28908  ax5seglem2  28909  axcontlem4  28947  ewlkprop  29584  uspgr2wlkeq  29626  uhgrwkspthlem2  29734  clwlkclwwlkfo  29988  eupth2lem3lem7  30213  frgr3vlem2  30253  3cyclfrgrrn1  30264  4cycl2vnunb  30269  frgrncvvdeqlem8  30285  grpoidinvlem3  30485  isvciOLD  30559  nmcvcn  30674  ipval2lem2  30683  sspimsval  30717  isblo2  30762  nmoo0  30770  blocni  30784  isph  30801  hvadd4  31015  hiassdi  31070  ocsh  31262  chj4  31514  spansncol  31547  pjjsi  31679  hoscl  31724  hodcl  31726  hoadd4  31763  homco1  31780  homulass  31781  hoadddi  31782  hoadddir  31783  unoplin  31899  adjvalval  31916  hmoplin  31921  bralnfn  31927  brafnmul  31930  lnopmi  31979  lnopcoi  31982  hmops  31999  hmopm  32000  nmophmi  32010  lnfncnbd  32036  cnlnadjlem2  32047  adjlnop  32065  adjmul  32071  adjadd  32072  branmfn  32084  kbass5  32099  kbass6  32100  leop2  32103  leopadd  32111  leopmuli  32112  pjimai  32155  atcvatlem  32364  chirredlem2  32370  mdsymlem3  32384  mdsymlem5  32386  sumdmdii  32394  sumdmdlem  32397  cdj3lem2a  32415  cdj3lem2b  32416  cdj3lem3a  32418  cdj3i  32420  nn0difffzod  32779  xreceu  32892  cshwrnid  32933  toslublem  32944  tosglblem  32946  lmodvslmhm  33033  archiabllem1b  33161  archiabllem2c  33164  archiabl  33167  slmdvsdir  33185  slmdvsass  33186  grplsm0l  33367  pidlnzb  33386  rprmndvdsru  33493  zarcls1  33852  pstmxmet  33880  ordtconnlem1  33907  hasheuni  34068  omsf  34280  ballotlemirc  34516  signswmnd  34541  bnj1204  34995  fineqvac  35080  fisshasheq  35095  revpfxsfxrev  35096  txpconn  35212  cvmscld  35253  satfbrsuc  35346  satfrnmapom  35350  satfun  35391  elmpps  35553  dfrdg2  35776  wsuclem  35806  segconeu  35992  linecom  36131  linethru  36134  lineintmo  36138  fnemeet2  36348  fnejoin2  36350  fvineqsneq  37393  lindsadd  37600  lindsdom  37601  lindsenlbs  37602  matunitlindflem1  37603  matunitlindflem2  37604  heicant  37642  mblfinlem1  37644  mblfinlem3  37646  ismblfin  37648  cnambfre  37655  itg2addnclem2  37659  ftc1anclem1  37680  ftc1anclem5  37684  ftc1anclem6  37685  ftc2nc  37689  areacirclem2  37696  areacirclem4  37698  areacirclem5  37699  areacirc  37700  fzmul  37728  subspopn  37739  isbndx  37769  isbnd2  37770  isbnd3  37771  ssbnd  37775  prdstotbnd  37781  heibor1  37797  rrnmet  37816  rngonegmn1l  37928  rngohomco  37961  rngoisocnv  37968  rngoisoco  37969  crngohomfo  37993  isidlc  38002  rngoidl  38011  prnc  38054  ispridlc  38057  cvrval2  39260  glbconxN  39365  hlrelat5N  39388  cvratlem  39408  cvrat2  39416  athgt  39443  3dim2  39455  llnn0  39503  lplnn0N  39534  lvoln0N  39578  snatpsubN  39737  paddasslem18  39824  pmod1i  39835  lhpexle2  39997  lhpexle3lem  39998  lhpexle3  39999  ldilcnv  40102  trlcnv  40152  trlnidatb  40164  cdleme32snaw  40422  cdleme32fvaw  40426  cdleme42ke  40472  cdlemeg46gf  40520  cdleme50trn12  40539  cdlemg1cex  40575  cdlemb3  40593  tgrpgrplem  40736  tgrpabl  40738  tendoplcl2  40765  tendo0pl  40778  tendoicl  40783  tendoipl  40784  cdlemkid3N  40920  tendoex  40962  erngdvlem4  40978  erngdvlem4-rN  40986  dib1dim  41152  dib1dim2  41155  dihglbcpreN  41287  dihmeetALTN  41314  dih1dimatlem  41316  dihatlat  41321  lcmineqlem1  42010  lcmineqlem3  42012  aks4d1p1  42057  aks4d1p7d1  42063  aks4d1p8  42068  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones17  42144  sticksstones19  42146  oddcomabszz  42926  acongtr  42960  rpnnen3lem  43013  islssfg  43052  lmhmfgsplit  43068  unxpwdom3  43077  hbtlem7  43107  iocmbl  43195  ss2iundf  43641  ismnu  44243  grumnudlem  44267  ismnushort  44283  nzss  44299  dvconstbi  44316  bccbc  44327  uzmptshftfval  44328  iccdifprioo  45507  climisp  45737  limsupresxr  45757  liminfresxr  45758  dvnmul  45934  volico  45974  volioore  45981  fourierdlem74  46171  fourierdlem75  46172  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0xp  46420  hspmbllem2  46618  smflimlem3  46764  smfsupmpt  46806  smfinflem  46808  smfinfmpt  46810  smflimsupmpt  46820  smfliminfmpt  46823  funressnbrafv2  47238  uniimaelsetpreimafv  47390  imasetpreimafvbijlemfv1  47397  imasetpreimafvbijlemfo  47399  sprsymrelfo  47491  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  grtrissvtx  47936  gricgrlic  48003  nn0mnd  48160  lcoss  48418  snlindsntorlem  48452  mreclat  48978  aacllem  49783