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  3189  vtocl3  3546  spc3egv  3582  moi2  3699  sbc3ie  3843  2if2  4556  preq12bg  4829  ralxfrd2  5382  reuhypd  5389  otsndisj  5494  funcnvqp  6599  fvtp1g  7189  fntpb  7200  f1imass  7256  weisoeq  7347  f1ofveu  7397  f1ocnvfv3  7398  funeldmdif  8045  curry1f  8103  curry2f  8105  funsssuppss  8187  frrlem13  8295  tfrlem11  8400  oalimcl  8570  oeordsuc  8604  oelim2  8605  nneob  8666  nadd4  8708  mapxpen  9155  findcard  9175  enfii  9198  domtrfil  9204  domnsymfi  9212  phplem2  9217  php  9219  wemaplem3  9560  en2eqpr  10019  infxpabs  10223  infxp  10226  cfflb  10271  cfsmolem  10282  isf32lem12  10376  fin1a2lem9  10420  fin1a2s  10426  axcc3  10450  axdc3lem4  10465  zornn0g  10517  pwfseqlem4  10674  tskwun  10796  tskint  10797  tskxp  10799  tskmap  10800  gruf  10823  grutsk1  10833  addcanpi  10911  ltapi  10915  mul4  11401  add4  11454  2addsub  11494  addsubeq4  11495  muladd  11667  ltleadd  11718  receu  11880  p1le  12084  mulgt1  12101  lbinf  12193  zdiv  12661  fzind  12689  fnn0ind  12690  fzindd  12693  uzss  12873  zbtwnre  12960  qmulcl  12981  qreccl  12983  xrlttr  13154  xaddass  13263  xmulasslem3  13300  xadddilem  13308  xrsupsslem  13321  xrinfmsslem  13322  supxrunb1  13333  ioo0  13385  ico0  13406  ioc0  13407  icc0  13408  iooshf  13441  prunioo  13496  ioojoin  13498  elfz5  13531  elfz0fzfz0  13648  elfzonelfzo  13783  fzind2  13799  mulexpz  14118  expsub  14126  digit1  14253  facndiv  14304  faclbnd4lem4  14312  faclbnd4  14313  faclbnd5  14314  bccmpl  14325  bcval5  14334  bcpasc  14337  hashunx  14402  hashunsnggt  14410  hashdmpropge2  14499  ccatrn  14605  swrdspsleq  14681  swrdccat2  14685  ccatpfx  14717  pfxccat1  14718  swrdswrd  14721  cshf1  14826  crim  15132  absmax  15346  ello12r  15531  elo12r  15542  climshftlem  15588  2sumeq2dv  15719  hash2iun  15837  expcnv  15878  2cprodeq2dv  15939  rpnnen2lem7  16236  dvdsval3  16274  dvdsnegb  16291  muldvds1  16298  muldvds2  16299  dvdscmul  16300  dvdsmulc  16301  dvdsmulcr  16303  dvds2ln  16306  divalgb  16421  ndvdssub  16426  gcddiv  16568  lcmfval  16638  lcmfcl  16645  dvdslcmf  16648  rpexp1i  16740  phiprmpw  16793  hashgcdeq  16807  pythagtriplem1  16834  pockthg  16924  infpnlem1  16928  4sqlem3  16968  0ramcl  17041  firest  17444  imasaddfnlem  17540  imasleval  17553  mrerintcl  17607  iscatd  17683  fullestrcsetc  18161  fullsetcestrc  18176  clatleglb  18526  mreclatBAD  18571  pslem  18580  mndind  18804  grplmulf1o  18994  grplactcnv  19024  mulgnn0subcl  19068  mulgsubcl  19069  mulgdir  19087  issubg2  19122  issubgrpd2  19123  nmzsubg  19146  eqgen  19162  cycsubm  19183  cycsubgcl  19187  cycsubgss  19188  ghmmulg  19209  ghmf1  19227  kerf1ghm  19228  conjghm  19230  symgpssefmnd  19375  gsmsymgreqlem2  19410  symgfixfo  19418  odeq  19529  odval2  19530  odf1  19541  dfod2  19543  gexdvds  19563  gexdvds2  19564  gexcl2  19568  gexdvds3  19569  sylow2blem2  19600  efgsp1  19716  efgrelexlemb  19729  cmnbascntr  19784  mulgmhm  19806  mulgghm  19807  iscyggen2  19860  iscyg3  19865  ablsimpgfindlem1  20088  srglmhm  20179  srgrmhm  20180  ringlghm  20270  ringrghm  20271  gsumdixp  20277  dvdsrcl2  20324  crngunit  20336  cntzsubrng  20525  subrgugrp  20549  cntzsubr  20564  rnghmsubcsetclem2  20590  rhmsubcsetclem2  20619  rhmsubcrngclem2  20625  sdrgacs  20759  lmodvsdir  20841  lmodvsass  20842  lmodvsghm  20878  lsssubg  20912  lss1d  20918  islbs2  21113  lidlsubg  21182  lidlsubcl  21183  rngqiprngimfo  21260  lpigen  21294  xrsdsreval  21377  expghm  21434  mulgghm2  21435  ip0r  21595  obs2ss  21687  islindf3  21784  scmatscm  22449  scmataddcl  22452  scmatsubcl  22453  scmatfo  22466  matunit  22614  cpmatelimp  22648  cpmatelimp2  22650  cpmatinvcl  22653  cpmatmcl  22655  mat2pmatf  22664  m2cpmf  22678  cpm2mf  22688  m2cpmfo  22692  m2cpminv  22696  decpmataa0  22704  pm2mpf  22734  pm2mpf1  22735  idpm2idmp  22737  pm2mpfo  22750  elcls2  23010  opnnei  23056  innei  23061  iscnp4  23199  cnpnei  23200  iscncl  23205  cnnei  23218  cnconst  23220  ordthauslem  23319  bwth  23346  1stccnp  23398  llyrest  23421  nllyrest  23422  kgenss  23479  xkoccn  23555  kqsat  23667  kqt0lem  23672  isr0  23673  fbssfi  23773  isfild  23794  filconn  23819  trfilss  23825  fgtr  23826  ufileu  23855  ufilen  23866  fmfnfmlem4  23893  fmfnfm  23894  hausflimi  23916  cnpflf2  23936  cnpflf  23937  cnpfcf  23977  cnextcn  24003  tsmsxplem1  24089  tsmsxp  24091  ustuqtop0  24177  ismeti  24262  isxmet2d  24264  elbl2ps  24326  elbl2  24327  xblpnfps  24332  xblpnf  24333  xbln0  24351  blin  24358  blssexps  24363  blssex  24364  blcls  24443  blsscls  24444  metrest  24461  metustbl  24503  psmetutop  24504  nmf2  24530  ngpi  24565  tngngp3  24593  nmdvr  24607  nmoi  24665  nmoix  24666  nmoleub  24668  nghmcn  24682  iccntr  24759  metdsle  24790  icoopnst  24885  iocopnst  24886  icccvx  24897  pi1xfr  25004  isclmi0  25047  iscvsi  25078  cphipval  25193  lmmbr  25208  lmmbr2  25209  iscfil3  25223  iscau2  25227  cfilres  25246  bcthlem1  25274  bcthlem4  25277  bcthlem5  25278  rrxmet  25358  ioombl  25516  iccvolcl  25518  ioovolcl  25521  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  ig1pcl  26134  ig1prsp  26136  aannenlem1  26286  taylplem1  26320  dvtaylp  26328  relogeftb  26543  logdivlt  26580  cxpexp  26627  rpcxpcl  26635  isppw2  27075  vmappw  27076  lgslem4  27261  lgscllem  27265  lgsneg1  27283  lgsne0  27296  nosepdm  27646  ssltdisj  27783  mulscutlem  28074  sltonold  28200  brbtwn2  28830  ax5seglem1  28853  ax5seglem2  28854  axcontlem4  28892  ewlkprop  29529  uspgr2wlkeq  29572  uhgrwkspthlem2  29682  clwlkclwwlkfo  29936  eupth2lem3lem7  30161  frgr3vlem2  30201  3cyclfrgrrn1  30212  4cycl2vnunb  30217  frgrncvvdeqlem8  30233  grpoidinvlem3  30433  isvciOLD  30507  nmcvcn  30622  ipval2lem2  30631  sspimsval  30665  isblo2  30710  nmoo0  30718  blocni  30732  isph  30749  hvadd4  30963  hiassdi  31018  ocsh  31210  chj4  31462  spansncol  31495  pjjsi  31627  hoscl  31672  hodcl  31674  hoadd4  31711  homco1  31728  homulass  31729  hoadddi  31730  hoadddir  31731  unoplin  31847  adjvalval  31864  hmoplin  31869  bralnfn  31875  brafnmul  31878  lnopmi  31927  lnopcoi  31930  hmops  31947  hmopm  31948  nmophmi  31958  lnfncnbd  31984  cnlnadjlem2  31995  adjlnop  32013  adjmul  32019  adjadd  32020  branmfn  32032  kbass5  32047  kbass6  32048  leop2  32051  leopadd  32059  leopmuli  32060  pjimai  32103  atcvatlem  32312  chirredlem2  32318  mdsymlem3  32332  mdsymlem5  32334  sumdmdii  32342  sumdmdlem  32345  cdj3lem2a  32363  cdj3lem2b  32364  cdj3lem3a  32366  cdj3i  32368  nn0difffzod  32729  xreceu  32842  cshwrnid  32883  toslublem  32898  tosglblem  32900  lmodvslmhm  32990  ogrpaddltbi  33032  archiabllem1b  33136  archiabllem2c  33139  archiabl  33142  slmdvsdir  33159  slmdvsass  33160  grplsm0l  33364  pidlnzb  33383  rprmndvdsru  33490  zarcls1  33846  pstmxmet  33874  ordtconnlem1  33901  hasheuni  34062  omsf  34274  ballotlemirc  34510  signswmnd  34535  bnj1204  34989  fineqvac  35074  fisshasheq  35083  revpfxsfxrev  35084  txpconn  35200  cvmscld  35241  satfbrsuc  35334  satfrnmapom  35338  satfun  35379  elmpps  35541  dfrdg2  35759  wsuclem  35789  segconeu  35975  linecom  36114  linethru  36117  lineintmo  36121  fnemeet2  36331  fnejoin2  36333  fvineqsneq  37376  lindsadd  37583  lindsdom  37584  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  heicant  37625  mblfinlem1  37627  mblfinlem3  37629  ismblfin  37631  cnambfre  37638  itg2addnclem2  37642  ftc1anclem1  37663  ftc1anclem5  37667  ftc1anclem6  37668  ftc2nc  37672  areacirclem2  37679  areacirclem4  37681  areacirclem5  37682  areacirc  37683  fzmul  37711  subspopn  37722  isbndx  37752  isbnd2  37753  isbnd3  37754  ssbnd  37758  prdstotbnd  37764  heibor1  37780  rrnmet  37799  rngonegmn1l  37911  rngohomco  37944  rngoisocnv  37951  rngoisoco  37952  crngohomfo  37976  isidlc  37985  rngoidl  37994  prnc  38037  ispridlc  38040  cvrval2  39238  glbconxN  39343  hlrelat5N  39366  cvratlem  39386  cvrat2  39394  athgt  39421  3dim2  39433  llnn0  39481  lplnn0N  39512  lvoln0N  39556  snatpsubN  39715  paddasslem18  39802  pmod1i  39813  lhpexle2  39975  lhpexle3lem  39976  lhpexle3  39977  ldilcnv  40080  trlcnv  40130  trlnidatb  40142  cdleme32snaw  40400  cdleme32fvaw  40404  cdleme42ke  40450  cdlemeg46gf  40498  cdleme50trn12  40517  cdlemg1cex  40553  cdlemb3  40571  tgrpgrplem  40714  tgrpabl  40716  tendoplcl2  40743  tendo0pl  40756  tendoicl  40761  tendoipl  40762  cdlemkid3N  40898  tendoex  40940  erngdvlem4  40956  erngdvlem4-rN  40964  dib1dim  41130  dib1dim2  41133  dihglbcpreN  41265  dihmeetALTN  41292  dih1dimatlem  41294  dihatlat  41299  lcmineqlem1  41988  lcmineqlem3  41990  aks4d1p1  42035  aks4d1p7d1  42041  aks4d1p8  42046  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones8  42112  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones12  42117  sticksstones17  42122  sticksstones19  42124  metakunt29  42192  metakunt30  42193  metakunt31  42194  factwoffsmonot  42201  oddcomabszz  42915  acongtr  42949  rpnnen3lem  43002  islssfg  43041  lmhmfgsplit  43057  unxpwdom3  43066  hbtlem7  43096  iocmbl  43184  ss2iundf  43630  ismnu  44233  grumnudlem  44257  ismnushort  44273  nzss  44289  dvconstbi  44306  bccbc  44317  uzmptshftfval  44318  iccdifprioo  45493  climisp  45723  limsupresxr  45743  liminfresxr  45744  dvnmul  45920  volico  45960  volioore  45967  fourierdlem74  46157  fourierdlem75  46158  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0xp  46406  hspmbllem2  46604  smflimlem3  46750  smfsupmpt  46792  smfinflem  46794  smfinfmpt  46796  smflimsupmpt  46806  smfliminfmpt  46809  funressnbrafv2  47221  uniimaelsetpreimafv  47358  imasetpreimafvbijlemfv1  47365  imasetpreimafvbijlemfo  47367  sprsymrelfo  47459  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  grtrissvtx  47904  gricgrlic  47971  nn0mnd  48102  lcoss  48360  snlindsntorlem  48394  mreclat  48919  aacllem  49613