Theorem 3expa 1132

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1133 and pm3.2an3 1355 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 1101	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbir 237	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-3an 1101

This theorem is referenced by:  3exp  1133  ad4ant123  1187  ad4ant124  1188  ad4ant134  1189  ad4ant234  1190  ad5ant123  1380  ad5ant124  1381  ad5ant125  1383  3anidm23  1441  mp3an2  1471  mpd3an3  1484  rgen3  3208  vtocl3  3533  spc3egv  3563  moi2  3680  sbc3ie  3822  2if2  4537  preq12bg  4812  ralxfrd2  5370  reuhypd  5377  otsndisj  5489  funcnvqp  6586  fvtp1g  7183  fntpb  7194  f1imass  7249  weisoeq  7340  f1ofveu  7391  f1ocnvfv3  7392  funeldmdif  8030  curry1f  8086  curry2f  8088  funsssuppss  8171  frrlem13  8280  tfrlem11  8360  oalimcl  8530  oeordsuc  8565  oelim2  8566  nneob  8627  nadd4  8670  mapxpen  9116  findcard  9133  enfii  9155  domtrfil  9161  domnsymfi  9169  phplem2  9174  php  9176  wemaplem3  9497  en2eqpr  9964  infxpabs  10168  infxp  10171  cfflb  10217  cfsmolem  10228  isf32lem12  10322  fin1a2lem9  10366  fin1a2s  10372  axcc3  10396  axdc3lem4  10411  zornn0g  10463  pwfseqlem4  10621  tskwun  10743  tskint  10744  tskxp  10746  tskmap  10747  gruf  10770  grutsk1  10780  addcanpi  10858  ltapi  10862  mul4  11352  add4  11405  2addsub  11445  addsubeq4  11446  muladd  11620  ltleadd  11671  receu  11833  p1le  12037  mulgt1  12054  lbinf  12146  zdiv  12644  fzind  12672  fnn0ind  12673  fzindd  12676  uzss  12863  zbtwnre  12948  qmulcl  12969  qreccl  12971  xrlttr  13143  xaddass  13253  xmulasslem3  13290  xadddilem  13298  xrsupsslem  13311  xrinfmsslem  13312  supxrunb1  13323  ioo0  13375  ico0  13396  ioc0  13397  icc0  13398  iooshf  13431  prunioo  13486  ioojoin  13488  elfz5  13522  elfz0fzfz0  13639  elfzonelfzo  13776  fzind2  13795  modaddb  13920  mulexpz  14116  expsub  14124  digit1  14251  facndiv  14302  faclbnd4lem4  14310  faclbnd4  14311  faclbnd5  14312  bccmpl  14323  bcval5  14332  bcpasc  14335  hashunx  14400  hashunsnggt  14408  hashdmpropge2  14497  ccatrn  14604  swrdspsleq  14680  swrdccat2  14684  ccatpfx  14715  pfxccat1  14716  swrdswrd  14719  cshf1  14824  crim  15143  absmax  15358  ello12r  15545  elo12r  15556  climshftlem  15602  2sumeq2dv  15733  hash2iun  15852  expcnv  15895  2cprodeq2dv  15956  rpnnen2lem7  16253  dvdsval3  16291  dvdsnegb  16308  muldvds1  16315  muldvds2  16316  dvdscmul  16317  dvdsmulc  16318  dvdsmulcr  16320  dvds2ln  16324  divalgb  16439  ndvdssub  16444  gcddiv  16586  lcmfval  16656  lcmfcl  16663  dvdslcmf  16666  rpexp1i  16759  phiprmpw  16812  hashgcdeq  16826  pythagtriplem1  16853  pockthg  16943  infpnlem1  16947  4sqlem3  16987  0ramcl  17060  firest  17462  imasaddfnlem  17559  imasleval  17572  mrerintcl  17626  iscatd  17706  fullestrcsetc  18184  fullsetcestrc  18199  clatleglb  18551  mreclatBAD  18596  pslem  18605  mndind  18863  grplmulf1o  19056  grplactcnv  19086  mulgnn0subcl  19130  mulgsubcl  19131  mulgdir  19149  issubg2  19184  issubgrpd2  19185  nmzsubg  19207  eqgen  19223  cycsubm  19244  cycsubgcl  19248  cycsubgss  19249  ghmmulg  19269  ghmf1  19287  kerf1ghm  19288  conjghm  19290  symgpssefmnd  19437  gsmsymgreqlem2  19472  symgfixfo  19480  odeq  19591  odval2  19592  odf1  19603  dfod2  19605  gexdvds  19625  gexdvds2  19626  gexcl2  19630  gexdvds3  19631  sylow2blem2  19662  efgsp1  19778  efgrelexlemb  19791  cmnbascntr  19846  mulgmhm  19868  mulgghm  19869  iscyggen2  19922  iscyg3  19927  ablsimpgfindlem1  20150  ogrpaddltbi  20180  srglmhm  20272  srgrmhm  20273  ringlghm  20363  ringrghm  20364  gsumdixp  20368  dvdsrcl2  20416  crngunit  20428  cntzsubrng  20618  subrgugrp  20642  cntzsubr  20657  rnghmsubcsetclem2  20683  rhmsubcsetclem2  20712  rhmsubcrngclem2  20718  sdrgacs  20851  lmodvsdir  20954  lmodvsass  20955  lmodvsghm  20991  lsssubg  21025  lss1d  21031  islbs2  21225  lidlsubg  21294  lidlsubcl  21295  rngqiprngimfo  21372  lpigen  21406  xrsdsreval  21465  expghm  21528  mulgghm2  21529  ip0r  21690  obs2ss  21782  islindf3  21879  scmatscm  22574  scmataddcl  22577  scmatsubcl  22578  scmatfo  22591  matunit  22739  cpmatelimp  22773  cpmatelimp2  22775  cpmatinvcl  22778  cpmatmcl  22780  mat2pmatf  22789  m2cpmf  22803  cpm2mf  22813  m2cpmfo  22817  m2cpminv  22821  decpmataa0  22829  pm2mpf  22859  pm2mpf1  22860  idpm2idmp  22862  pm2mpfo  22875  elcls2  23135  opnnei  23181  innei  23186  iscnp4  23324  cnpnei  23325  iscncl  23330  cnnei  23343  cnconst  23345  ordthauslem  23444  bwth  23471  1stccnp  23523  llyrest  23546  nllyrest  23547  kgenss  23604  xkoccn  23680  kqsat  23792  kqt0lem  23797  isr0  23798  fbssfi  23898  isfild  23919  filconn  23944  trfilss  23950  fgtr  23951  ufileu  23980  ufilen  23991  fmfnfmlem4  24018  fmfnfm  24019  hausflimi  24041  cnpflf2  24061  cnpflf  24062  cnpfcf  24102  cnextcn  24128  tsmsxplem1  24214  tsmsxp  24216  ustuqtop0  24301  ismeti  24386  isxmet2d  24388  elbl2ps  24450  elbl2  24451  xblpnfps  24456  xblpnf  24457  xbln0  24475  blin  24482  blssexps  24487  blssex  24488  blcls  24567  blsscls  24568  metrest  24585  metustbl  24627  psmetutop  24628  nmf2  24654  ngpi  24689  tngngp3  24717  nmdvr  24731  nmoi  24789  nmoix  24790  nmoleub  24792  nghmcn  24806  iccntr  24883  metdsle  24914  icoopnst  25002  iocopnst  25003  icccvx  25013  pi1xfr  25118  isclmi0  25161  iscvsi  25192  cphipval  25306  lmmbr  25321  lmmbr2  25322  iscfil3  25336  iscau2  25340  cfilres  25359  bcthlem1  25387  bcthlem4  25390  bcthlem5  25391  rrxmet  25471  ioombl  25628  iccvolcl  25630  ioovolcl  25633  mbfi1fseqlem3  25780  mbfi1fseqlem4  25781  mbfi1fseqlem5  25782  ig1pcl  26240  ig1prsp  26242  aannenlem1  26393  taylplem1  26427  dvtaylp  26434  relogeftb  26650  logdivlt  26687  cxpexp  26734  rpcxpcl  26742  isppw2  27180  vmappw  27181  lgslem4  27365  lgscllem  27369  lgsneg1  27387  lgsne0  27400  nosepdm  27749  sltsdisj  27897  mulcutlem  28225  ltonold  28355  zsoring  28503  bdayfinbndlem1  28561  z12bdaylem  28578  brbtwn2  29107  ax5seglem1  29130  ax5seglem2  29131  axcontlem4  29169  ewlkprop  29805  uspgr2wlkeq  29847  uhgrwkspthlem2  29955  clwlkclwwlkfo  30212  eupth2lem3lem7  30437  frgr3vlem2  30477  3cyclfrgrrn1  30488  4cycl2vnunb  30493  frgrncvvdeqlem8  30509  grpoidinvlem3  30710  isvciOLD  30784  nmcvcn  30899  ipval2lem2  30908  sspimsval  30942  isblo2  30987  nmoo0  30995  blocni  31009  isph  31026  hvadd4  31240  hiassdi  31295  ocsh  31487  chj4  31739  spansncol  31772  pjjsi  31904  hoscl  31949  hodcl  31951  hoadd4  31988  homco1  32005  homulass  32006  hoadddi  32007  hoadddir  32008  unoplin  32124  adjvalval  32141  hmoplin  32146  bralnfn  32152  brafnmul  32155  lnopmi  32204  lnopcoi  32207  hmops  32224  hmopm  32225  nmophmi  32235  lnfncnbd  32261  cnlnadjlem2  32272  adjlnop  32290  adjmul  32296  adjadd  32297  branmfn  32309  kbass5  32324  kbass6  32325  leop2  32328  leopadd  32336  leopmuli  32337  pjimai  32380  atcvatlem  32589  chirredlem2  32595  mdsymlem3  32609  mdsymlem5  32611  sumdmdii  32619  sumdmdlem  32622  cdj3lem2a  32640  cdj3lem2b  32641  cdj3lem3a  32643  cdj3i  32645  nn0difffzod  33007  xreceu  33100  cshwrnid  33140  toslublem  33151  tosglblem  33153  lmodvslmhm  33231  archiabllem1b  33373  archiabllem2c  33376  archiabl  33379  slmdvsdir  33397  slmdvsass  33398  grplsm0l  33590  pidlnzb  33609  rprmndvdsru  33726  mplvrpmmhm  33844  mplvrpmrhm  33845  zarcls1  34167  pstmxmet  34195  ordtconnlem1  34222  hasheuni  34383  omsf  34594  ballotlemirc  34830  signswmnd  34852  bnj1204  35308  fineqvac  35413  fisshasheq  35466  revpfxsfxrev  35467  txpconn  35583  cvmscld  35624  satfbrsuc  35717  satfrnmapom  35721  satfun  35762  elmpps  35924  dfrdg2  36144  wsuclem  36174  segconeu  36362  linecom  36501  linethru  36504  lineintmo  36508  fnemeet2  36728  fnejoin2  36730  fvineqsneq  37907  lindsadd  38113  lindsdom  38114  lindsenlbs  38115  matunitlindflem1  38116  matunitlindflem2  38117  heicant  38155  mblfinlem1  38157  mblfinlem3  38159  ismblfin  38161  cnambfre  38168  itg2addnclem2  38172  ftc1anclem1  38193  ftc1anclem5  38197  ftc1anclem6  38198  ftc2nc  38202  areacirclem2  38209  areacirclem4  38211  areacirclem5  38212  areacirc  38213  fzmul  38241  subspopn  38252  isbndx  38282  isbnd2  38283  isbnd3  38284  ssbnd  38288  prdstotbnd  38294  heibor1  38310  rrnmet  38329  rngonegmn1l  38441  rngohomco  38474  rngoisocnv  38481  rngoisoco  38482  crngohomfo  38506  isidlc  38515  rngoidl  38524  prnc  38567  ispridlc  38570  cvrval2  39899  glbconxN  40003  hlrelat5N  40026  cvratlem  40046  cvrat2  40054  athgt  40081  3dim2  40093  llnn0  40141  lplnn0N  40172  lvoln0N  40216  snatpsubN  40375  paddasslem18  40462  pmod1i  40473  lhpexle2  40635  lhpexle3lem  40636  lhpexle3  40637  ldilcnv  40740  trlcnv  40790  trlnidatb  40802  cdleme32snaw  41060  cdleme32fvaw  41064  cdleme42ke  41110  cdlemeg46gf  41158  cdleme50trn12  41177  cdlemg1cex  41213  cdlemb3  41231  tgrpgrplem  41374  tgrpabl  41376  tendoplcl2  41403  tendo0pl  41416  tendoicl  41421  tendoipl  41422  cdlemkid3N  41558  tendoex  41600  erngdvlem4  41616  erngdvlem4-rN  41624  dib1dim  41790  dib1dim2  41793  dihglbcpreN  41925  dihmeetALTN  41952  dih1dimatlem  41954  dihatlat  41959  lcmineqlem1  42647  lcmineqlem3  42649  aks4d1p1  42694  aks4d1p7d1  42700  aks4d1p8  42705  sticksstones1  42764  sticksstones2  42765  sticksstones3  42766  sticksstones8  42771  sticksstones10  42773  sticksstones11  42774  sticksstones12a  42775  sticksstones12  42776  sticksstones17  42781  sticksstones19  42783  oddcomabszz  43522  acongtr  43556  rpnnen3lem  43609  islssfg  43648  lmhmfgsplit  43664  unxpwdom3  43673  hbtlem7  43703  iocmbl  43791  ss2iundf  44236  ismnu  44838  grumnudlem  44862  ismnushort  44878  nzss  44894  dvconstbi  44911  bccbc  44922  uzmptshftfval  44923  iccdifprioo  46093  climisp  46321  limsupresxr  46341  liminfresxr  46342  dvnmul  46518  volico  46558  volioore  46565  fourierdlem74  46755  fourierdlem75  46756  sge0iunmptlemfi  46988  sge0iunmptlemre  46990  sge0iunmpt  46993  sge0xp  47004  hspmbllem2  47202  smflimlem3  47348  smfsupmpt  47390  smfinflem  47392  smfinfmpt  47394  smflimsupmpt  47404  smfliminfmpt  47407  funressnbrafv2  47839  uniimaelsetpreimafv  48003  imasetpreimafvbijlemfv1  48010  imasetpreimafvbijlemfo  48012  sprsymrelfo  48104  nnsum4primesodd  48419  nnsum4primesoddALTV  48420  grtrissvtx  48567  gricgrlic  48641  nn0mnd  48802  lcoss  49059  snlindsntorlem  49093  mreclat  49619  aacllem  50423