Theorem 3expa 1117

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1118 and pm3.2an3 1339 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  1118  ad4ant123  1171  ad4ant124  1172  ad4ant134  1173  ad4ant234  1174  ad5ant123  1363  3anidm23  1420  mp3an2  1448  mpd3an3  1461  rgen3  3201  vtocl3  3566  spc3egv  3602  moi2  3724  sbc3ie  3876  2if2  4585  preq12bg  4857  ralxfrd2  5417  reuhypd  5424  otsndisj  5528  funcnvqp  6631  fvtp1g  7217  fntpb  7228  f1imass  7283  weisoeq  7374  f1ofveu  7424  f1ocnvfv3  7425  funeldmdif  8071  curry1f  8129  curry2f  8131  funsssuppss  8213  frrlem13  8321  tfrlem11  8426  oalimcl  8596  oeordsuc  8630  oelim2  8631  nneob  8692  nadd4  8734  mapxpen  9181  findcard  9201  enfii  9223  domtrfil  9229  domnsymfi  9237  phplem2  9242  php  9244  wemaplem3  9585  en2eqpr  10044  infxpabs  10248  infxp  10251  cfflb  10296  cfsmolem  10307  isf32lem12  10401  fin1a2lem9  10445  fin1a2s  10451  axcc3  10475  axdc3lem4  10490  zornn0g  10542  pwfseqlem4  10699  tskwun  10821  tskint  10822  tskxp  10824  tskmap  10825  gruf  10848  grutsk1  10858  addcanpi  10936  ltapi  10940  mul4  11426  add4  11479  2addsub  11519  addsubeq4  11520  muladd  11692  ltleadd  11743  receu  11905  p1le  12109  mulgt1  12126  lbinf  12218  zdiv  12685  fzind  12713  fnn0ind  12714  fzindd  12717  uzss  12898  zbtwnre  12985  qmulcl  13006  qreccl  13008  xrlttr  13178  xaddass  13287  xmulasslem3  13324  xadddilem  13332  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  ioo0  13408  ico0  13429  ioc0  13430  icc0  13431  iooshf  13462  prunioo  13517  ioojoin  13519  elfz5  13552  elfz0fzfz0  13669  elfzonelfzo  13804  fzind2  13820  mulexpz  14139  expsub  14147  digit1  14272  facndiv  14323  faclbnd4lem4  14331  faclbnd4  14332  faclbnd5  14333  bccmpl  14344  bcval5  14353  bcpasc  14356  hashunx  14421  hashunsnggt  14429  hashdmpropge2  14518  ccatrn  14623  swrdspsleq  14699  swrdccat2  14703  ccatpfx  14735  pfxccat1  14736  swrdswrd  14739  cshf1  14844  crim  15150  absmax  15364  ello12r  15549  elo12r  15560  climshftlem  15606  2sumeq2dv  15737  hash2iun  15855  expcnv  15896  2cprodeq2dv  15957  rpnnen2lem7  16252  dvdsval3  16290  dvdsnegb  16307  muldvds1  16314  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  dvdsmulcr  16319  dvds2ln  16322  divalgb  16437  ndvdssub  16442  gcddiv  16584  lcmfval  16654  lcmfcl  16661  dvdslcmf  16664  rpexp1i  16756  phiprmpw  16809  hashgcdeq  16822  pythagtriplem1  16849  pockthg  16939  infpnlem1  16943  4sqlem3  16983  0ramcl  17056  firest  17478  imasaddfnlem  17574  imasleval  17587  mrerintcl  17641  iscatd  17717  fullestrcsetc  18206  fullsetcestrc  18221  clatleglb  18575  mreclatBAD  18620  pslem  18629  mndind  18853  grplmulf1o  19043  grplactcnv  19073  mulgnn0subcl  19117  mulgsubcl  19118  mulgdir  19136  issubg2  19171  issubgrpd2  19172  nmzsubg  19195  eqgen  19211  cycsubm  19232  cycsubgcl  19236  cycsubgss  19237  ghmmulg  19258  ghmf1  19276  kerf1ghm  19277  conjghm  19279  symgpssefmnd  19427  gsmsymgreqlem2  19463  symgfixfo  19471  odeq  19582  odval2  19583  odf1  19594  dfod2  19596  gexdvds  19616  gexdvds2  19617  gexcl2  19621  gexdvds3  19622  sylow2blem2  19653  efgsp1  19769  efgrelexlemb  19782  cmnbascntr  19837  mulgmhm  19859  mulgghm  19860  iscyggen2  19913  iscyg3  19918  ablsimpgfindlem1  20141  srglmhm  20238  srgrmhm  20239  ringlghm  20325  ringrghm  20326  gsumdixp  20332  dvdsrcl2  20382  crngunit  20394  cntzsubrng  20583  subrgugrp  20607  cntzsubr  20622  rnghmsubcsetclem2  20648  rhmsubcsetclem2  20677  rhmsubcrngclem2  20683  sdrgacs  20818  lmodvsdir  20900  lmodvsass  20901  lmodvsghm  20937  lsssubg  20972  lss1d  20978  islbs2  21173  lidlsubg  21250  lidlsubcl  21251  rngqiprngimfo  21328  lpigen  21362  xrsdsreval  21446  expghm  21503  mulgghm2  21504  ip0r  21672  obs2ss  21766  islindf3  21863  scmatscm  22534  scmataddcl  22537  scmatsubcl  22538  scmatfo  22551  matunit  22699  cpmatelimp  22733  cpmatelimp2  22735  cpmatinvcl  22738  cpmatmcl  22740  mat2pmatf  22749  m2cpmf  22763  cpm2mf  22773  m2cpmfo  22777  m2cpminv  22781  decpmataa0  22789  pm2mpf  22819  pm2mpf1  22820  idpm2idmp  22822  pm2mpfo  22835  elcls2  23097  opnnei  23143  innei  23148  iscnp4  23286  cnpnei  23287  iscncl  23292  cnnei  23305  cnconst  23307  ordthauslem  23406  bwth  23433  1stccnp  23485  llyrest  23508  nllyrest  23509  kgenss  23566  xkoccn  23642  kqsat  23754  kqt0lem  23759  isr0  23760  fbssfi  23860  isfild  23881  filconn  23906  trfilss  23912  fgtr  23913  ufileu  23942  ufilen  23953  fmfnfmlem4  23980  fmfnfm  23981  hausflimi  24003  cnpflf2  24023  cnpflf  24024  cnpfcf  24064  cnextcn  24090  tsmsxplem1  24176  tsmsxp  24178  ustuqtop0  24264  ismeti  24350  isxmet2d  24352  elbl2ps  24414  elbl2  24415  xblpnfps  24420  xblpnf  24421  xbln0  24439  blin  24446  blssexps  24451  blssex  24452  blcls  24534  blsscls  24535  metrest  24552  metustbl  24594  psmetutop  24595  nmf2  24621  ngpi  24656  tngngp3  24692  nmdvr  24706  nmoi  24764  nmoix  24765  nmoleub  24767  nghmcn  24781  iccntr  24856  metdsle  24887  icoopnst  24982  iocopnst  24983  icccvx  24994  pi1xfr  25101  isclmi0  25144  iscvsi  25175  cphipval  25290  lmmbr  25305  lmmbr2  25306  iscfil3  25320  iscau2  25324  cfilres  25343  bcthlem1  25371  bcthlem4  25374  bcthlem5  25375  rrxmet  25455  ioombl  25613  iccvolcl  25615  ioovolcl  25618  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  ig1pcl  26232  ig1prsp  26234  aannenlem1  26384  taylplem1  26418  dvtaylp  26426  relogeftb  26640  logdivlt  26677  cxpexp  26724  rpcxpcl  26732  isppw2  27172  vmappw  27173  lgslem4  27358  lgscllem  27362  lgsneg1  27380  lgsne0  27393  nosepdm  27743  ssltdisj  27880  mulscutlem  28171  sltonold  28297  brbtwn2  28934  ax5seglem1  28957  ax5seglem2  28958  axcontlem4  28996  ewlkprop  29635  uspgr2wlkeq  29678  uhgrwkspthlem2  29786  clwlkclwwlkfo  30037  eupth2lem3lem7  30262  frgr3vlem2  30302  3cyclfrgrrn1  30313  4cycl2vnunb  30318  frgrncvvdeqlem8  30334  grpoidinvlem3  30534  isvciOLD  30608  nmcvcn  30723  ipval2lem2  30732  sspimsval  30766  isblo2  30811  nmoo0  30819  blocni  30833  isph  30850  hvadd4  31064  hiassdi  31119  ocsh  31311  chj4  31563  spansncol  31596  pjjsi  31728  hoscl  31773  hodcl  31775  hoadd4  31812  homco1  31829  homulass  31830  hoadddi  31831  hoadddir  31832  unoplin  31948  adjvalval  31965  hmoplin  31970  bralnfn  31976  brafnmul  31979  lnopmi  32028  lnopcoi  32031  hmops  32048  hmopm  32049  nmophmi  32059  lnfncnbd  32085  cnlnadjlem2  32096  adjlnop  32114  adjmul  32120  adjadd  32121  branmfn  32133  kbass5  32148  kbass6  32149  leop2  32152  leopadd  32160  leopmuli  32161  pjimai  32204  atcvatlem  32413  chirredlem2  32419  mdsymlem3  32433  mdsymlem5  32435  sumdmdii  32443  sumdmdlem  32446  cdj3lem2a  32464  cdj3lem2b  32465  cdj3lem3a  32467  cdj3i  32469  nn0difffzod  32813  xreceu  32888  cshwrnid  32930  toslublem  32946  tosglblem  32948  lmodvslmhm  33035  ogrpaddltbi  33077  archiabllem1b  33181  archiabllem2c  33184  archiabl  33187  slmdvsdir  33204  slmdvsass  33205  grplsm0l  33410  pidlnzb  33429  rprmndvdsru  33536  zarcls1  33829  pstmxmet  33857  ordtconnlem1  33884  hasheuni  34065  omsf  34277  ballotlemirc  34512  signswmnd  34550  bnj1204  35004  fineqvac  35089  fisshasheq  35098  revpfxsfxrev  35099  txpconn  35216  cvmscld  35257  satfbrsuc  35350  satfrnmapom  35354  satfun  35395  elmpps  35557  dfrdg2  35776  wsuclem  35806  segconeu  35992  linecom  36131  linethru  36134  lineintmo  36138  fnemeet2  36349  fnejoin2  36351  fvineqsneq  37394  lindsadd  37599  lindsdom  37600  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  heicant  37641  mblfinlem1  37643  mblfinlem3  37645  ismblfin  37647  cnambfre  37654  itg2addnclem2  37658  ftc1anclem1  37679  ftc1anclem5  37683  ftc1anclem6  37684  ftc2nc  37688  areacirclem2  37695  areacirclem4  37697  areacirclem5  37698  areacirc  37699  fzmul  37727  subspopn  37738  isbndx  37768  isbnd2  37769  isbnd3  37770  ssbnd  37774  prdstotbnd  37780  heibor1  37796  rrnmet  37815  rngonegmn1l  37927  rngohomco  37960  rngoisocnv  37967  rngoisoco  37968  crngohomfo  37992  isidlc  38001  rngoidl  38010  prnc  38053  ispridlc  38056  cvrval2  39255  glbconxN  39360  hlrelat5N  39383  cvratlem  39403  cvrat2  39411  athgt  39438  3dim2  39450  llnn0  39498  lplnn0N  39529  lvoln0N  39573  snatpsubN  39732  paddasslem18  39819  pmod1i  39830  lhpexle2  39992  lhpexle3lem  39993  lhpexle3  39994  ldilcnv  40097  trlcnv  40147  trlnidatb  40159  cdleme32snaw  40417  cdleme32fvaw  40421  cdleme42ke  40467  cdlemeg46gf  40515  cdleme50trn12  40534  cdlemg1cex  40570  cdlemb3  40588  tgrpgrplem  40731  tgrpabl  40733  tendoplcl2  40760  tendo0pl  40773  tendoicl  40778  tendoipl  40779  cdlemkid3N  40915  tendoex  40957  erngdvlem4  40973  erngdvlem4-rN  40981  dib1dim  41147  dib1dim2  41150  dihglbcpreN  41282  dihmeetALTN  41309  dih1dimatlem  41311  dihatlat  41316  lcmineqlem1  42010  lcmineqlem3  42012  aks4d1p1  42057  aks4d1p7d1  42063  aks4d1p8  42068  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones17  42144  sticksstones19  42146  metakunt29  42214  metakunt30  42215  metakunt31  42216  factwoffsmonot  42223  oddcomabszz  42932  acongtr  42966  rpnnen3lem  43019  islssfg  43058  lmhmfgsplit  43074  unxpwdom3  43083  hbtlem7  43113  iocmbl  43201  ss2iundf  43648  ismnu  44256  grumnudlem  44280  ismnushort  44296  nzss  44312  dvconstbi  44329  bccbc  44340  uzmptshftfval  44341  iccdifprioo  45468  climisp  45701  limsupresxr  45721  liminfresxr  45722  dvnmul  45898  volico  45938  volioore  45945  fourierdlem74  46135  fourierdlem75  46136  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0xp  46384  hspmbllem2  46582  smflimlem3  46728  smfsupmpt  46770  smfinflem  46772  smfinfmpt  46774  smflimsupmpt  46784  smfliminfmpt  46787  funressnbrafv2  47193  uniimaelsetpreimafv  47320  imasetpreimafvbijlemfv1  47327  imasetpreimafvbijlemfo  47329  sprsymrelfo  47421  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  uspgrimprop  47810  grtrissvtx  47848  gricgrlic  47913  nn0mnd  48022  lcoss  48281  snlindsntorlem  48315  mreclat  48785  aacllem  49031