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  3174  vtocl3  3522  spc3egv  3558  moi2  3676  sbc3ie  3820  2if2  4532  preq12bg  4804  ralxfrd2  5351  reuhypd  5358  otsndisj  5462  funcnvqp  6546  fvtp1g  7134  fntpb  7145  f1imass  7201  weisoeq  7292  f1ofveu  7343  f1ocnvfv3  7344  funeldmdif  7983  curry1f  8039  curry2f  8041  funsssuppss  8123  frrlem13  8231  tfrlem11  8310  oalimcl  8478  oeordsuc  8512  oelim2  8513  nneob  8574  nadd4  8616  mapxpen  9060  findcard  9077  enfii  9100  domtrfil  9106  domnsymfi  9114  phplem2  9119  php  9121  wemaplem3  9440  en2eqpr  9901  infxpabs  10105  infxp  10108  cfflb  10153  cfsmolem  10164  isf32lem12  10258  fin1a2lem9  10302  fin1a2s  10308  axcc3  10332  axdc3lem4  10347  zornn0g  10399  pwfseqlem4  10556  tskwun  10678  tskint  10679  tskxp  10681  tskmap  10682  gruf  10705  grutsk1  10715  addcanpi  10793  ltapi  10797  mul4  11284  add4  11337  2addsub  11377  addsubeq4  11378  muladd  11552  ltleadd  11603  receu  11765  p1le  11969  mulgt1  11986  lbinf  12078  zdiv  12546  fzind  12574  fnn0ind  12575  fzindd  12578  uzss  12758  zbtwnre  12847  qmulcl  12868  qreccl  12870  xrlttr  13042  xaddass  13151  xmulasslem3  13188  xadddilem  13196  xrsupsslem  13209  xrinfmsslem  13210  supxrunb1  13221  ioo0  13273  ico0  13294  ioc0  13295  icc0  13296  iooshf  13329  prunioo  13384  ioojoin  13386  elfz5  13419  elfz0fzfz0  13536  elfzonelfzo  13672  fzind2  13688  modaddb  13813  mulexpz  14009  expsub  14017  digit1  14144  facndiv  14195  faclbnd4lem4  14203  faclbnd4  14204  faclbnd5  14205  bccmpl  14216  bcval5  14225  bcpasc  14228  hashunx  14293  hashunsnggt  14301  hashdmpropge2  14390  ccatrn  14496  swrdspsleq  14572  swrdccat2  14576  ccatpfx  14607  pfxccat1  14608  swrdswrd  14611  cshf1  14716  crim  15022  absmax  15237  ello12r  15424  elo12r  15435  climshftlem  15481  2sumeq2dv  15612  hash2iun  15730  expcnv  15771  2cprodeq2dv  15832  rpnnen2lem7  16129  dvdsval3  16167  dvdsnegb  16184  muldvds1  16191  muldvds2  16192  dvdscmul  16193  dvdsmulc  16194  dvdsmulcr  16196  dvds2ln  16200  divalgb  16315  ndvdssub  16320  gcddiv  16462  lcmfval  16532  lcmfcl  16539  dvdslcmf  16542  rpexp1i  16634  phiprmpw  16687  hashgcdeq  16701  pythagtriplem1  16728  pockthg  16818  infpnlem1  16822  4sqlem3  16862  0ramcl  16935  firest  17336  imasaddfnlem  17432  imasleval  17445  mrerintcl  17499  iscatd  17579  fullestrcsetc  18057  fullsetcestrc  18072  clatleglb  18424  mreclatBAD  18469  pslem  18478  mndind  18702  grplmulf1o  18892  grplactcnv  18922  mulgnn0subcl  18966  mulgsubcl  18967  mulgdir  18985  issubg2  19020  issubgrpd2  19021  nmzsubg  19044  eqgen  19060  cycsubm  19081  cycsubgcl  19085  cycsubgss  19086  ghmmulg  19107  ghmf1  19125  kerf1ghm  19126  conjghm  19128  symgpssefmnd  19275  gsmsymgreqlem2  19310  symgfixfo  19318  odeq  19429  odval2  19430  odf1  19441  dfod2  19443  gexdvds  19463  gexdvds2  19464  gexcl2  19468  gexdvds3  19469  sylow2blem2  19500  efgsp1  19616  efgrelexlemb  19629  cmnbascntr  19684  mulgmhm  19706  mulgghm  19707  iscyggen2  19760  iscyg3  19765  ablsimpgfindlem1  19988  ogrpaddltbi  20018  srglmhm  20106  srgrmhm  20107  ringlghm  20197  ringrghm  20198  gsumdixp  20204  dvdsrcl2  20251  crngunit  20263  cntzsubrng  20452  subrgugrp  20476  cntzsubr  20491  rnghmsubcsetclem2  20517  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  sdrgacs  20686  lmodvsdir  20789  lmodvsass  20790  lmodvsghm  20826  lsssubg  20860  lss1d  20866  islbs2  21061  lidlsubg  21130  lidlsubcl  21131  rngqiprngimfo  21208  lpigen  21242  xrsdsreval  21318  expghm  21382  mulgghm2  21383  ip0r  21544  obs2ss  21636  islindf3  21733  scmatscm  22398  scmataddcl  22401  scmatsubcl  22402  scmatfo  22415  matunit  22563  cpmatelimp  22597  cpmatelimp2  22599  cpmatinvcl  22602  cpmatmcl  22604  mat2pmatf  22613  m2cpmf  22627  cpm2mf  22637  m2cpmfo  22641  m2cpminv  22645  decpmataa0  22653  pm2mpf  22683  pm2mpf1  22684  idpm2idmp  22686  pm2mpfo  22699  elcls2  22959  opnnei  23005  innei  23010  iscnp4  23148  cnpnei  23149  iscncl  23154  cnnei  23167  cnconst  23169  ordthauslem  23268  bwth  23295  1stccnp  23347  llyrest  23370  nllyrest  23371  kgenss  23428  xkoccn  23504  kqsat  23616  kqt0lem  23621  isr0  23622  fbssfi  23722  isfild  23743  filconn  23768  trfilss  23774  fgtr  23775  ufileu  23804  ufilen  23815  fmfnfmlem4  23842  fmfnfm  23843  hausflimi  23865  cnpflf2  23885  cnpflf  23886  cnpfcf  23926  cnextcn  23952  tsmsxplem1  24038  tsmsxp  24040  ustuqtop0  24126  ismeti  24211  isxmet2d  24213  elbl2ps  24275  elbl2  24276  xblpnfps  24281  xblpnf  24282  xbln0  24300  blin  24307  blssexps  24312  blssex  24313  blcls  24392  blsscls  24393  metrest  24410  metustbl  24452  psmetutop  24453  nmf2  24479  ngpi  24514  tngngp3  24542  nmdvr  24556  nmoi  24614  nmoix  24615  nmoleub  24617  nghmcn  24631  iccntr  24708  metdsle  24739  icoopnst  24834  iocopnst  24835  icccvx  24846  pi1xfr  24953  isclmi0  24996  iscvsi  25027  cphipval  25141  lmmbr  25156  lmmbr2  25157  iscfil3  25171  iscau2  25175  cfilres  25194  bcthlem1  25222  bcthlem4  25225  bcthlem5  25226  rrxmet  25306  ioombl  25464  iccvolcl  25466  ioovolcl  25469  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  ig1pcl  26082  ig1prsp  26084  aannenlem1  26234  taylplem1  26268  dvtaylp  26276  relogeftb  26491  logdivlt  26528  cxpexp  26575  rpcxpcl  26583  isppw2  27023  vmappw  27024  lgslem4  27209  lgscllem  27213  lgsneg1  27231  lgsne0  27244  nosepdm  27594  ssltdisj  27734  mulscutlem  28039  sltonold  28167  zsoring  28301  brbtwn2  28850  ax5seglem1  28873  ax5seglem2  28874  axcontlem4  28912  ewlkprop  29549  uspgr2wlkeq  29591  uhgrwkspthlem2  29699  clwlkclwwlkfo  29953  eupth2lem3lem7  30178  frgr3vlem2  30218  3cyclfrgrrn1  30229  4cycl2vnunb  30234  frgrncvvdeqlem8  30250  grpoidinvlem3  30450  isvciOLD  30524  nmcvcn  30639  ipval2lem2  30648  sspimsval  30682  isblo2  30727  nmoo0  30735  blocni  30749  isph  30766  hvadd4  30980  hiassdi  31035  ocsh  31227  chj4  31479  spansncol  31512  pjjsi  31644  hoscl  31689  hodcl  31691  hoadd4  31728  homco1  31745  homulass  31746  hoadddi  31747  hoadddir  31748  unoplin  31864  adjvalval  31881  hmoplin  31886  bralnfn  31892  brafnmul  31895  lnopmi  31944  lnopcoi  31947  hmops  31964  hmopm  31965  nmophmi  31975  lnfncnbd  32001  cnlnadjlem2  32012  adjlnop  32030  adjmul  32036  adjadd  32037  branmfn  32049  kbass5  32064  kbass6  32065  leop2  32068  leopadd  32076  leopmuli  32077  pjimai  32120  atcvatlem  32329  chirredlem2  32335  mdsymlem3  32349  mdsymlem5  32351  sumdmdii  32359  sumdmdlem  32362  cdj3lem2a  32380  cdj3lem2b  32381  cdj3lem3a  32383  cdj3i  32385  nn0difffzod  32750  xreceu  32863  cshwrnid  32904  toslublem  32915  tosglblem  32917  lmodvslmhm  33004  archiabllem1b  33135  archiabllem2c  33138  archiabl  33141  slmdvsdir  33159  slmdvsass  33160  grplsm0l  33341  pidlnzb  33360  rprmndvdsru  33467  mplvrpmmhm  33549  zarcls1  33842  pstmxmet  33870  ordtconnlem1  33897  hasheuni  34058  omsf  34270  ballotlemirc  34506  signswmnd  34531  bnj1204  34985  fineqvac  35078  fisshasheq  35098  revpfxsfxrev  35099  txpconn  35215  cvmscld  35256  satfbrsuc  35349  satfrnmapom  35353  satfun  35394  elmpps  35556  dfrdg2  35779  wsuclem  35809  segconeu  35995  linecom  36134  linethru  36137  lineintmo  36141  fnemeet2  36351  fnejoin2  36353  fvineqsneq  37396  lindsadd  37603  lindsdom  37604  lindsenlbs  37605  matunitlindflem1  37606  matunitlindflem2  37607  heicant  37645  mblfinlem1  37647  mblfinlem3  37649  ismblfin  37651  cnambfre  37658  itg2addnclem2  37662  ftc1anclem1  37683  ftc1anclem5  37687  ftc1anclem6  37688  ftc2nc  37692  areacirclem2  37699  areacirclem4  37701  areacirclem5  37702  areacirc  37703  fzmul  37731  subspopn  37742  isbndx  37772  isbnd2  37773  isbnd3  37774  ssbnd  37778  prdstotbnd  37784  heibor1  37800  rrnmet  37819  rngonegmn1l  37931  rngohomco  37964  rngoisocnv  37971  rngoisoco  37972  crngohomfo  37996  isidlc  38005  rngoidl  38014  prnc  38057  ispridlc  38060  cvrval2  39263  glbconxN  39367  hlrelat5N  39390  cvratlem  39410  cvrat2  39418  athgt  39445  3dim2  39457  llnn0  39505  lplnn0N  39536  lvoln0N  39580  snatpsubN  39739  paddasslem18  39826  pmod1i  39837  lhpexle2  39999  lhpexle3lem  40000  lhpexle3  40001  ldilcnv  40104  trlcnv  40154  trlnidatb  40166  cdleme32snaw  40424  cdleme32fvaw  40428  cdleme42ke  40474  cdlemeg46gf  40522  cdleme50trn12  40541  cdlemg1cex  40577  cdlemb3  40595  tgrpgrplem  40738  tgrpabl  40740  tendoplcl2  40767  tendo0pl  40780  tendoicl  40785  tendoipl  40786  cdlemkid3N  40922  tendoex  40964  erngdvlem4  40980  erngdvlem4-rN  40988  dib1dim  41154  dib1dim2  41157  dihglbcpreN  41289  dihmeetALTN  41316  dih1dimatlem  41318  dihatlat  41323  lcmineqlem1  42012  lcmineqlem3  42014  aks4d1p1  42059  aks4d1p7d1  42065  aks4d1p8  42070  sticksstones1  42129  sticksstones2  42130  sticksstones3  42131  sticksstones8  42136  sticksstones10  42138  sticksstones11  42139  sticksstones12a  42140  sticksstones12  42141  sticksstones17  42146  sticksstones19  42148  oddcomabszz  42927  acongtr  42961  rpnnen3lem  43014  islssfg  43053  lmhmfgsplit  43069  unxpwdom3  43078  hbtlem7  43108  iocmbl  43196  ss2iundf  43642  ismnu  44244  grumnudlem  44268  ismnushort  44284  nzss  44300  dvconstbi  44317  bccbc  44328  uzmptshftfval  44329  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  47938  gricgrlic  48012  nn0mnd  48173  lcoss  48431  snlindsntorlem  48465  mreclat  48991  aacllem  49796