Theorem 3expa 1113

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

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

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 1084

This theorem is referenced by:  3exp  1114  ad4ant123  1167  ad4ant124  1168  ad4ant134  1169  ad4ant234  1170  ad5ant123  1359  3anidm23  1416  mp3an2  1443  mpd3an3  1456  rgen3  3202  vtocl3  3562  spc3egv  3602  moi2  3705  sbc3ie  3850  2if2  4518  preq12bg  4776  ralxfrd2  5303  reuhypd  5310  otsndisj  5400  funcnvqp  6411  fvtp1g  6953  fntpb  6964  f1imass  7014  weisoeq  7100  f1ofveu  7143  f1ocnvfv3  7144  funeldmdif  7739  curry1f  7793  curry2f  7795  funsssuppss  7848  tfrlem11  8016  oalimcl  8178  oeordsuc  8212  oelim2  8213  nneob  8271  mapxpen  8675  findcard  8749  wemaplem3  9004  en2eqpr  9425  infxpabs  9626  infxp  9629  cfflb  9673  cfsmolem  9684  isf32lem12  9778  fin1a2lem9  9822  fin1a2s  9828  axcc3  9852  axdc3lem4  9867  zornn0g  9919  pwfseqlem4  10076  tskwun  10198  tskint  10199  tskxp  10201  tskmap  10202  gruf  10225  grutsk1  10235  addcanpi  10313  ltapi  10317  mul4  10800  add4  10852  2addsub  10892  addsubeq4  10893  muladd  11064  ltleadd  11115  receu  11277  p1le  11477  lbinf  11586  zdiv  12044  fzind  12072  fnn0ind  12073  uzss  12257  zbtwnre  12338  qmulcl  12358  qreccl  12360  xrlttr  12525  xaddass  12634  xmulasslem3  12671  xadddilem  12679  xrsupsslem  12692  xrinfmsslem  12693  supxrunb1  12704  ioo0  12755  ico0  12776  ioc0  12777  icc0  12778  iooshf  12807  prunioo  12859  ioojoin  12861  elfz5  12892  elfz0fzfz0  13004  elfzonelfzo  13131  fzind2  13147  mulexpz  13461  expsub  13469  digit1  13590  facndiv  13640  faclbnd4lem4  13648  faclbnd4  13649  faclbnd5  13650  bccmpl  13661  bcval5  13670  bcpasc  13673  hashunx  13739  hashunsnggt  13747  hashdmpropge2  13833  ccatrn  13935  swrdspsleq  14019  swrdccat2  14023  ccatpfx  14055  pfxccat1  14056  swrdswrd  14059  cshf1  14164  crim  14466  absmax  14681  ello12r  14866  elo12r  14877  climshftlem  14923  2sumeq2dv  15054  hash2iun  15170  expcnv  15211  2cprodeq2dv  15271  rpnnen2lem7  15565  dvdsval3  15603  dvdsnegb  15619  muldvds1  15626  muldvds2  15627  dvdscmul  15628  dvdsmulc  15629  dvdsmulcr  15631  dvds2ln  15634  divalgb  15747  ndvdssub  15752  gcddiv  15891  lcmfval  15957  lcmfcl  15964  dvdslcmf  15967  rpexp1i  16057  phiprmpw  16105  hashgcdeq  16118  pythagtriplem1  16145  pockthg  16234  infpnlem1  16238  4sqlem3  16278  0ramcl  16351  firest  16698  imasaddfnlem  16793  imasleval  16806  mrerintcl  16860  iscatd  16936  fullestrcsetc  17393  fullsetcestrc  17408  clatleglb  17728  mreclatBAD  17789  pslem  17808  mndind  17984  grplmulf1o  18165  grplactcnv  18194  mulgnn0subcl  18233  mulgsubcl  18234  mulgdir  18251  issubg2  18286  issubgrpd2  18287  nmzsubg  18309  eqgen  18325  cycsubm  18337  cycsubgcl  18341  cycsubgss  18342  ghmmulg  18362  conjghm  18381  symgpssefmnd  18516  gsmsymgreqlem2  18551  symgfixfo  18559  odeq  18670  odval2  18671  odf1  18681  dfod2  18683  gexdvds  18701  gexdvds2  18702  gexcl2  18706  gexdvds3  18707  sylow2blem2  18738  efgsp1  18855  efgrelexlemb  18868  mulgmhm  18940  mulgghm  18941  iscyggen2  18992  iscyg3  18997  ablsimpgfindlem1  19221  srglmhm  19277  srgrmhm  19278  ringlghm  19346  ringrghm  19347  gsumdixp  19351  dvdsrcl2  19392  crngunit  19404  kerf1ghm  19489  kerf1hrmOLD  19490  subrgugrp  19546  cntzsubr  19560  sdrgacs  19572  lmodvsdir  19650  lmodvsass  19651  lmodvsghm  19687  lsssubg  19721  lss1d  19727  islbs2  19918  lidlsubg  19980  lidlsubcl  19981  quscrng  20005  lpigen  20021  xrsdsreval  20582  expghm  20635  mulgghm2  20636  ip0r  20773  obs2ss  20865  islindf3  20962  scmatscm  21114  scmataddcl  21117  scmatsubcl  21118  scmatfo  21131  matunit  21279  cpmatelimp  21312  cpmatelimp2  21314  cpmatinvcl  21317  cpmatmcl  21319  mat2pmatf  21328  m2cpmf  21342  cpm2mf  21352  m2cpmfo  21356  m2cpminv  21360  decpmataa0  21368  pm2mpf  21398  pm2mpf1  21399  idpm2idmp  21401  pm2mpfo  21414  elcls2  21674  opnnei  21720  innei  21725  iscnp4  21863  cnpnei  21864  iscncl  21869  cnnei  21882  cnconst  21884  ordthauslem  21983  bwth  22010  1stccnp  22062  llyrest  22085  nllyrest  22086  kgenss  22143  xkoccn  22219  kqsat  22331  kqt0lem  22336  isr0  22337  fbssfi  22437  isfild  22458  filconn  22483  trfilss  22489  fgtr  22490  ufileu  22519  ufilen  22530  fmfnfmlem4  22557  fmfnfm  22558  hausflimi  22580  cnpflf2  22600  cnpflf  22601  cnpfcf  22641  cnextcn  22667  tsmsxplem1  22753  tsmsxp  22755  ustuqtop0  22841  ismeti  22927  isxmet2d  22929  elbl2ps  22991  elbl2  22992  xblpnfps  22997  xblpnf  22998  xbln0  23016  blin  23023  blssexps  23028  blssex  23029  blcls  23108  blsscls  23109  metrest  23126  metustbl  23168  psmetutop  23169  nmf2  23194  ngpi  23229  tngngp3  23257  nmdvr  23271  nmoi  23329  nmoix  23330  nmoleub  23332  nghmcn  23346  iccntr  23421  metdsle  23452  icoopnst  23535  iocopnst  23536  icccvx  23546  pi1xfr  23651  isclmi0  23694  iscvsi  23725  cphipval  23838  lmmbr  23853  lmmbr2  23854  iscfil3  23868  iscau2  23872  cfilres  23891  bcthlem1  23919  bcthlem4  23922  bcthlem5  23923  rrxmet  24003  ioombl  24158  iccvolcl  24160  ioovolcl  24163  mbfi1fseqlem3  24310  mbfi1fseqlem4  24311  mbfi1fseqlem5  24312  ig1pcl  24761  ig1prsp  24763  aannenlem1  24909  taylplem1  24943  dvtaylp  24950  relogeftb  25160  logdivlt  25196  cxpexp  25243  rpcxpcl  25251  isppw2  25684  vmappw  25685  lgslem4  25868  lgscllem  25872  lgsneg1  25890  lgsne0  25903  brbtwn2  26683  ax5seglem1  26706  ax5seglem2  26707  axcontlem4  26745  ewlkprop  27377  uspgr2wlkeq  27419  uhgrwkspthlem2  27527  clwlkclwwlkfo  27779  eupth2lem3lem7  28005  frgr3vlem2  28045  3cyclfrgrrn1  28056  4cycl2vnunb  28061  frgrncvvdeqlem8  28077  grpoidinvlem3  28275  isvciOLD  28349  nmcvcn  28464  ipval2lem2  28473  sspimsval  28507  isblo2  28552  nmoo0  28560  blocni  28574  isph  28591  hvadd4  28805  hiassdi  28860  ocsh  29052  chj4  29304  spansncol  29337  pjjsi  29469  hoscl  29514  hodcl  29516  hoadd4  29553  homco1  29570  homulass  29571  hoadddi  29572  hoadddir  29573  unoplin  29689  adjvalval  29706  hmoplin  29711  bralnfn  29717  brafnmul  29720  lnopmi  29769  lnopcoi  29772  hmops  29789  hmopm  29790  nmophmi  29800  lnfncnbd  29826  cnlnadjlem2  29837  adjlnop  29855  adjmul  29861  adjadd  29862  branmfn  29874  kbass5  29889  kbass6  29890  leop2  29893  leopadd  29901  leopmuli  29902  pjimai  29945  atcvatlem  30154  chirredlem2  30160  mdsymlem3  30174  mdsymlem5  30176  sumdmdii  30184  sumdmdlem  30187  cdj3lem2a  30205  cdj3lem2b  30206  cdj3lem3a  30208  cdj3i  30210  xreceu  30591  cshwrnid  30628  toslublem  30647  tosglblem  30649  lmodvslmhm  30681  ogrpaddltbi  30712  archiabllem1b  30814  archiabllem2c  30817  archiabl  30820  slmdvsdir  30837  slmdvsass  30838  pstmxmet  31130  ordtconnlem1  31160  hasheuni  31337  omsf  31547  ballotlemirc  31782  signswmnd  31820  bnj1204  32277  fisshasheq  32345  revpfxsfxrev  32355  txpconn  32472  cvmscld  32513  satfbrsuc  32606  satfrnmapom  32610  satfun  32651  elmpps  32813  dfrdg2  33033  wsuclem  33105  frrlem13  33128  nosepdm  33181  segconeu  33465  linecom  33604  linethru  33607  lineintmo  33611  fnemeet2  33708  fnejoin2  33710  fvineqsneq  34685  lindsadd  34877  lindsdom  34878  lindsenlbs  34879  matunitlindflem1  34880  matunitlindflem2  34881  heicant  34919  mblfinlem1  34921  mblfinlem3  34923  ismblfin  34925  cnambfre  34932  itg2addnclem2  34936  ftc1anclem1  34959  ftc1anclem5  34963  ftc1anclem6  34964  ftc2nc  34968  areacirclem2  34975  areacirclem4  34977  areacirclem5  34978  areacirc  34979  fzmul  35008  subspopn  35019  isbndx  35052  isbnd2  35053  isbnd3  35054  ssbnd  35058  prdstotbnd  35064  heibor1  35080  rrnmet  35099  rngonegmn1l  35211  rngohomco  35244  rngoisocnv  35251  rngoisoco  35252  crngohomfo  35276  isidlc  35285  rngoidl  35294  prnc  35337  ispridlc  35340  cvrval2  36402  glbconxN  36506  hlrelat5N  36529  cvratlem  36549  cvrat2  36557  athgt  36584  3dim2  36596  llnn0  36644  lplnn0N  36675  lvoln0N  36719  snatpsubN  36878  paddasslem18  36965  pmod1i  36976  lhpexle2  37138  lhpexle3lem  37139  lhpexle3  37140  ldilcnv  37243  trlcnv  37293  trlnidatb  37305  cdleme32snaw  37563  cdleme32fvaw  37567  cdleme42ke  37613  cdlemeg46gf  37661  cdleme50trn12  37680  cdlemg1cex  37716  cdlemb3  37734  tgrpgrplem  37877  tgrpabl  37879  tendoplcl2  37906  tendo0pl  37919  tendoicl  37924  tendoipl  37925  cdlemkid3N  38061  tendoex  38103  erngdvlem4  38119  erngdvlem4-rN  38127  dib1dim  38293  dib1dim2  38296  dihglbcpreN  38428  dihmeetALTN  38455  dih1dimatlem  38457  dihatlat  38462  oddcomabszz  39532  acongtr  39566  rpnnen3lem  39619  islssfg  39661  lmhmfgsplit  39677  unxpwdom3  39686  hbtlem7  39716  iocmbl  39810  ss2iundf  39995  ismnu  40588  grumnudlem  40612  nzss  40640  dvconstbi  40657  bccbc  40668  uzmptshftfval  40669  iccdifprioo  41782  climisp  42017  limsupresxr  42037  liminfresxr  42038  dvnmul  42218  volico  42259  volioore  42266  fourierdlem74  42456  fourierdlem75  42457  sge0iunmptlemfi  42686  sge0iunmptlemre  42688  sge0iunmpt  42691  sge0xp  42702  hspmbllem2  42900  smflimlem3  43040  smfsupmpt  43080  smfinflem  43082  smfinfmpt  43084  smflimsupmpt  43094  smfliminfmpt  43097  funressnbrafv2  43434  uniimaelsetpreimafv  43547  imasetpreimafvbijlemfv1  43554  imasetpreimafvbijlemfo  43556  sprsymrelfo  43650  nnsum4primesodd  43952  nnsum4primesoddALTV  43953  nn0mnd  44077  rnghmsubcsetclem2  44238  rhmsubcsetclem2  44284  rhmsubcrngclem2  44290  lcoss  44482  snlindsntorlem  44516  aacllem  44893