Theorem 3expa 1114

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 1085

This theorem is referenced by:  3exp  1115  ad4ant123  1168  ad4ant124  1169  ad4ant134  1170  ad4ant234  1171  ad5ant123  1360  3anidm23  1417  mp3an2  1445  mpd3an3  1458  rgen3  3204  vtocl3  3563  spc3egv  3603  moi2  3706  sbc3ie  3851  2if2  4519  preq12bg  4777  ralxfrd2  5304  reuhypd  5311  otsndisj  5401  funcnvqp  6412  fvtp1g  6954  fntpb  6966  f1imass  7016  weisoeq  7102  f1ofveu  7145  f1ocnvfv3  7146  funeldmdif  7741  curry1f  7795  curry2f  7797  funsssuppss  7850  tfrlem11  8018  oalimcl  8180  oeordsuc  8214  oelim2  8215  nneob  8273  mapxpen  8677  findcard  8751  wemaplem3  9006  en2eqpr  9427  infxpabs  9628  infxp  9631  cfflb  9675  cfsmolem  9686  isf32lem12  9780  fin1a2lem9  9824  fin1a2s  9830  axcc3  9854  axdc3lem4  9869  zornn0g  9921  pwfseqlem4  10078  tskwun  10200  tskint  10201  tskxp  10203  tskmap  10204  gruf  10227  grutsk1  10237  addcanpi  10315  ltapi  10319  mul4  10802  add4  10854  2addsub  10894  addsubeq4  10895  muladd  11066  ltleadd  11117  receu  11279  p1le  11479  lbinf  11588  zdiv  12046  fzind  12074  fnn0ind  12075  uzss  12259  zbtwnre  12340  qmulcl  12360  qreccl  12362  xrlttr  12527  xaddass  12636  xmulasslem3  12673  xadddilem  12681  xrsupsslem  12694  xrinfmsslem  12695  supxrunb1  12706  ioo0  12757  ico0  12778  ioc0  12779  icc0  12780  iooshf  12809  prunioo  12861  ioojoin  12863  elfz5  12894  elfz0fzfz0  13006  elfzonelfzo  13133  fzind2  13149  mulexpz  13463  expsub  13471  digit1  13592  facndiv  13642  faclbnd4lem4  13650  faclbnd4  13651  faclbnd5  13652  bccmpl  13663  bcval5  13672  bcpasc  13675  hashunx  13741  hashunsnggt  13749  hashdmpropge2  13835  ccatrn  13937  swrdspsleq  14021  swrdccat2  14025  ccatpfx  14057  pfxccat1  14058  swrdswrd  14061  cshf1  14166  crim  14468  absmax  14683  ello12r  14868  elo12r  14879  climshftlem  14925  2sumeq2dv  15056  hash2iun  15172  expcnv  15213  2cprodeq2dv  15273  rpnnen2lem7  15567  dvdsval3  15605  dvdsnegb  15621  muldvds1  15628  muldvds2  15629  dvdscmul  15630  dvdsmulc  15631  dvdsmulcr  15633  dvds2ln  15636  divalgb  15749  ndvdssub  15754  gcddiv  15893  lcmfval  15959  lcmfcl  15966  dvdslcmf  15969  rpexp1i  16059  phiprmpw  16107  hashgcdeq  16120  pythagtriplem1  16147  pockthg  16236  infpnlem1  16240  4sqlem3  16280  0ramcl  16353  firest  16700  imasaddfnlem  16795  imasleval  16808  mrerintcl  16862  iscatd  16938  fullestrcsetc  17395  fullsetcestrc  17410  clatleglb  17730  mreclatBAD  17791  pslem  17810  mndind  17986  grplmulf1o  18167  grplactcnv  18196  mulgnn0subcl  18235  mulgsubcl  18236  mulgdir  18253  issubg2  18288  issubgrpd2  18289  nmzsubg  18311  eqgen  18327  cycsubm  18339  cycsubgcl  18343  cycsubgss  18344  ghmmulg  18364  conjghm  18383  symgpssefmnd  18518  gsmsymgreqlem2  18553  symgfixfo  18561  odeq  18672  odval2  18673  odf1  18683  dfod2  18685  gexdvds  18703  gexdvds2  18704  gexcl2  18708  gexdvds3  18709  sylow2blem2  18740  efgsp1  18857  efgrelexlemb  18870  mulgmhm  18942  mulgghm  18943  iscyggen2  18994  iscyg3  18999  ablsimpgfindlem1  19223  srglmhm  19279  srgrmhm  19280  ringlghm  19348  ringrghm  19349  gsumdixp  19353  dvdsrcl2  19394  crngunit  19406  kerf1ghm  19491  kerf1hrmOLD  19492  subrgugrp  19548  cntzsubr  19562  sdrgacs  19574  lmodvsdir  19652  lmodvsass  19653  lmodvsghm  19689  lsssubg  19723  lss1d  19729  islbs2  19920  lidlsubg  19982  lidlsubcl  19983  quscrng  20007  lpigen  20023  xrsdsreval  20584  expghm  20637  mulgghm2  20638  ip0r  20775  obs2ss  20867  islindf3  20964  scmatscm  21116  scmataddcl  21119  scmatsubcl  21120  scmatfo  21133  matunit  21281  cpmatelimp  21314  cpmatelimp2  21316  cpmatinvcl  21319  cpmatmcl  21321  mat2pmatf  21330  m2cpmf  21344  cpm2mf  21354  m2cpmfo  21358  m2cpminv  21362  decpmataa0  21370  pm2mpf  21400  pm2mpf1  21401  idpm2idmp  21403  pm2mpfo  21416  elcls2  21676  opnnei  21722  innei  21727  iscnp4  21865  cnpnei  21866  iscncl  21871  cnnei  21884  cnconst  21886  ordthauslem  21985  bwth  22012  1stccnp  22064  llyrest  22087  nllyrest  22088  kgenss  22145  xkoccn  22221  kqsat  22333  kqt0lem  22338  isr0  22339  fbssfi  22439  isfild  22460  filconn  22485  trfilss  22491  fgtr  22492  ufileu  22521  ufilen  22532  fmfnfmlem4  22559  fmfnfm  22560  hausflimi  22582  cnpflf2  22602  cnpflf  22603  cnpfcf  22643  cnextcn  22669  tsmsxplem1  22755  tsmsxp  22757  ustuqtop0  22843  ismeti  22929  isxmet2d  22931  elbl2ps  22993  elbl2  22994  xblpnfps  22999  xblpnf  23000  xbln0  23018  blin  23025  blssexps  23030  blssex  23031  blcls  23110  blsscls  23111  metrest  23128  metustbl  23170  psmetutop  23171  nmf2  23196  ngpi  23231  tngngp3  23259  nmdvr  23273  nmoi  23331  nmoix  23332  nmoleub  23334  nghmcn  23348  iccntr  23423  metdsle  23454  icoopnst  23537  iocopnst  23538  icccvx  23548  pi1xfr  23653  isclmi0  23696  iscvsi  23727  cphipval  23840  lmmbr  23855  lmmbr2  23856  iscfil3  23870  iscau2  23874  cfilres  23893  bcthlem1  23921  bcthlem4  23924  bcthlem5  23925  rrxmet  24005  ioombl  24160  iccvolcl  24162  ioovolcl  24165  mbfi1fseqlem3  24312  mbfi1fseqlem4  24313  mbfi1fseqlem5  24314  ig1pcl  24763  ig1prsp  24765  aannenlem1  24911  taylplem1  24945  dvtaylp  24952  relogeftb  25162  logdivlt  25198  cxpexp  25245  rpcxpcl  25253  isppw2  25686  vmappw  25687  lgslem4  25870  lgscllem  25874  lgsneg1  25892  lgsne0  25905  brbtwn2  26685  ax5seglem1  26708  ax5seglem2  26709  axcontlem4  26747  ewlkprop  27379  uspgr2wlkeq  27421  uhgrwkspthlem2  27529  clwlkclwwlkfo  27781  eupth2lem3lem7  28007  frgr3vlem2  28047  3cyclfrgrrn1  28058  4cycl2vnunb  28063  frgrncvvdeqlem8  28079  grpoidinvlem3  28277  isvciOLD  28351  nmcvcn  28466  ipval2lem2  28475  sspimsval  28509  isblo2  28554  nmoo0  28562  blocni  28576  isph  28593  hvadd4  28807  hiassdi  28862  ocsh  29054  chj4  29306  spansncol  29339  pjjsi  29471  hoscl  29516  hodcl  29518  hoadd4  29555  homco1  29572  homulass  29573  hoadddi  29574  hoadddir  29575  unoplin  29691  adjvalval  29708  hmoplin  29713  bralnfn  29719  brafnmul  29722  lnopmi  29771  lnopcoi  29774  hmops  29791  hmopm  29792  nmophmi  29802  lnfncnbd  29828  cnlnadjlem2  29839  adjlnop  29857  adjmul  29863  adjadd  29864  branmfn  29876  kbass5  29891  kbass6  29892  leop2  29895  leopadd  29903  leopmuli  29904  pjimai  29947  atcvatlem  30156  chirredlem2  30162  mdsymlem3  30176  mdsymlem5  30178  sumdmdii  30186  sumdmdlem  30189  cdj3lem2a  30207  cdj3lem2b  30208  cdj3lem3a  30210  cdj3i  30212  xreceu  30593  cshwrnid  30630  toslublem  30649  tosglblem  30651  lmodvslmhm  30683  ogrpaddltbi  30714  archiabllem1b  30816  archiabllem2c  30819  archiabl  30822  slmdvsdir  30839  slmdvsass  30840  pstmxmet  31132  ordtconnlem1  31162  hasheuni  31339  omsf  31549  ballotlemirc  31784  signswmnd  31822  bnj1204  32279  fisshasheq  32347  revpfxsfxrev  32357  txpconn  32474  cvmscld  32515  satfbrsuc  32608  satfrnmapom  32612  satfun  32653  elmpps  32815  dfrdg2  33035  wsuclem  33107  frrlem13  33130  nosepdm  33183  segconeu  33467  linecom  33606  linethru  33609  lineintmo  33613  fnemeet2  33710  fnejoin2  33712  fvineqsneq  34687  lindsadd  34879  lindsdom  34880  lindsenlbs  34881  matunitlindflem1  34882  matunitlindflem2  34883  heicant  34921  mblfinlem1  34923  mblfinlem3  34925  ismblfin  34927  cnambfre  34934  itg2addnclem2  34938  ftc1anclem1  34961  ftc1anclem5  34965  ftc1anclem6  34966  ftc2nc  34970  areacirclem2  34977  areacirclem4  34979  areacirclem5  34980  areacirc  34981  fzmul  35010  subspopn  35021  isbndx  35054  isbnd2  35055  isbnd3  35056  ssbnd  35060  prdstotbnd  35066  heibor1  35082  rrnmet  35101  rngonegmn1l  35213  rngohomco  35246  rngoisocnv  35253  rngoisoco  35254  crngohomfo  35278  isidlc  35287  rngoidl  35296  prnc  35339  ispridlc  35342  cvrval2  36404  glbconxN  36508  hlrelat5N  36531  cvratlem  36551  cvrat2  36559  athgt  36586  3dim2  36598  llnn0  36646  lplnn0N  36677  lvoln0N  36721  snatpsubN  36880  paddasslem18  36967  pmod1i  36978  lhpexle2  37140  lhpexle3lem  37141  lhpexle3  37142  ldilcnv  37245  trlcnv  37295  trlnidatb  37307  cdleme32snaw  37565  cdleme32fvaw  37569  cdleme42ke  37615  cdlemeg46gf  37663  cdleme50trn12  37682  cdlemg1cex  37718  cdlemb3  37736  tgrpgrplem  37879  tgrpabl  37881  tendoplcl2  37908  tendo0pl  37921  tendoicl  37926  tendoipl  37927  cdlemkid3N  38063  tendoex  38105  erngdvlem4  38121  erngdvlem4-rN  38129  dib1dim  38295  dib1dim2  38298  dihglbcpreN  38430  dihmeetALTN  38457  dih1dimatlem  38459  dihatlat  38464  oddcomabszz  39534  acongtr  39568  rpnnen3lem  39621  islssfg  39663  lmhmfgsplit  39679  unxpwdom3  39688  hbtlem7  39718  iocmbl  39812  ss2iundf  39997  ismnu  40590  grumnudlem  40614  nzss  40642  dvconstbi  40659  bccbc  40670  uzmptshftfval  40671  iccdifprioo  41785  climisp  42020  limsupresxr  42040  liminfresxr  42041  dvnmul  42221  volico  42262  volioore  42269  fourierdlem74  42459  fourierdlem75  42460  sge0iunmptlemfi  42689  sge0iunmptlemre  42691  sge0iunmpt  42694  sge0xp  42705  hspmbllem2  42903  smflimlem3  43043  smfsupmpt  43083  smfinflem  43085  smfinfmpt  43087  smflimsupmpt  43097  smfliminfmpt  43100  funressnbrafv2  43437  uniimaelsetpreimafv  43550  imasetpreimafvbijlemfv1  43557  imasetpreimafvbijlemfo  43559  sprsymrelfo  43653  nnsum4primesodd  43955  nnsum4primesoddALTV  43956  nn0mnd  44080  rnghmsubcsetclem2  44241  rhmsubcsetclem2  44287  rhmsubcrngclem2  44293  lcoss  44485  snlindsntorlem  44519  aacllem  44896