Theorem 3expa 1119

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-3an 1090

This theorem is referenced by:  3exp  1120  ad4ant123  1173  ad4ant124  1174  ad4ant134  1175  ad4ant234  1176  ad5ant123  1365  3anidm23  1422  mp3an2  1450  mpd3an3  1463  rgen3  3203  vtocl3  3553  spc3egv  3594  moi2  3713  sbc3ie  3864  2if2  4584  preq12bg  4855  ralxfrd2  5411  reuhypd  5418  otsndisj  5520  funcnvqp  6613  fvtp1g  7199  fntpb  7211  f1imass  7263  weisoeq  7352  f1ofveu  7403  f1ocnvfv3  7404  funeldmdif  8034  curry1f  8092  curry2f  8094  funsssuppss  8175  frrlem13  8283  tfrlem11  8388  oalimcl  8560  oeordsuc  8594  oelim2  8595  nneob  8655  nadd4  8697  mapxpen  9143  findcard  9163  enfii  9189  domtrfil  9195  domnsymfi  9203  phplem2  9208  php  9210  wemaplem3  9543  en2eqpr  10002  infxpabs  10207  infxp  10210  cfflb  10254  cfsmolem  10265  isf32lem12  10359  fin1a2lem9  10403  fin1a2s  10409  axcc3  10433  axdc3lem4  10448  zornn0g  10500  pwfseqlem4  10657  tskwun  10779  tskint  10780  tskxp  10782  tskmap  10783  gruf  10806  grutsk1  10816  addcanpi  10894  ltapi  10898  mul4  11382  add4  11434  2addsub  11474  addsubeq4  11475  muladd  11646  ltleadd  11697  receu  11859  p1le  12059  lbinf  12167  zdiv  12632  fzind  12660  fnn0ind  12661  fzindd  12664  uzss  12845  zbtwnre  12930  qmulcl  12951  qreccl  12953  xrlttr  13119  xaddass  13228  xmulasslem3  13265  xadddilem  13273  xrsupsslem  13286  xrinfmsslem  13287  supxrunb1  13298  ioo0  13349  ico0  13370  ioc0  13371  icc0  13372  iooshf  13403  prunioo  13458  ioojoin  13460  elfz5  13493  elfz0fzfz0  13606  elfzonelfzo  13734  fzind2  13750  mulexpz  14068  expsub  14076  digit1  14200  facndiv  14248  faclbnd4lem4  14256  faclbnd4  14257  faclbnd5  14258  bccmpl  14269  bcval5  14278  bcpasc  14281  hashunx  14346  hashunsnggt  14354  hashdmpropge2  14444  ccatrn  14539  swrdspsleq  14615  swrdccat2  14619  ccatpfx  14651  pfxccat1  14652  swrdswrd  14655  cshf1  14760  crim  15062  absmax  15276  ello12r  15461  elo12r  15472  climshftlem  15518  2sumeq2dv  15651  hash2iun  15769  expcnv  15810  2cprodeq2dv  15869  rpnnen2lem7  16163  dvdsval3  16201  dvdsnegb  16217  muldvds1  16224  muldvds2  16225  dvdscmul  16226  dvdsmulc  16227  dvdsmulcr  16229  dvds2ln  16232  divalgb  16347  ndvdssub  16352  gcddiv  16493  lcmfval  16558  lcmfcl  16565  dvdslcmf  16568  rpexp1i  16660  phiprmpw  16709  hashgcdeq  16722  pythagtriplem1  16749  pockthg  16839  infpnlem1  16843  4sqlem3  16883  0ramcl  16956  firest  17378  imasaddfnlem  17474  imasleval  17487  mrerintcl  17541  iscatd  17617  fullestrcsetc  18103  fullsetcestrc  18118  clatleglb  18471  mreclatBAD  18516  pslem  18525  mndind  18709  grplmulf1o  18897  grplactcnv  18926  mulgnn0subcl  18967  mulgsubcl  18968  mulgdir  18986  issubg2  19021  issubgrpd2  19022  nmzsubg  19045  eqgen  19061  cycsubm  19079  cycsubgcl  19083  cycsubgss  19084  ghmmulg  19104  conjghm  19123  symgpssefmnd  19263  gsmsymgreqlem2  19299  symgfixfo  19307  odeq  19418  odval2  19419  odf1  19430  dfod2  19432  gexdvds  19452  gexdvds2  19453  gexcl2  19457  gexdvds3  19458  sylow2blem2  19489  efgsp1  19605  efgrelexlemb  19618  cmnbascntr  19673  mulgmhm  19695  mulgghm  19696  iscyggen2  19749  iscyg3  19754  ablsimpgfindlem1  19977  srglmhm  20044  srgrmhm  20045  ringlghm  20124  ringrghm  20125  gsumdixp  20131  dvdsrcl2  20180  crngunit  20192  kerf1ghm  20282  subrgugrp  20338  cntzsubr  20353  sdrgacs  20417  lmodvsdir  20496  lmodvsass  20497  lmodvsghm  20533  lsssubg  20568  lss1d  20574  islbs2  20767  lidlsubg  20838  lidlsubcl  20839  quscrng  20878  lpigen  20894  xrsdsreval  20990  expghm  21045  mulgghm2  21046  ip0r  21190  obs2ss  21284  islindf3  21381  scmatscm  22015  scmataddcl  22018  scmatsubcl  22019  scmatfo  22032  matunit  22180  cpmatelimp  22214  cpmatelimp2  22216  cpmatinvcl  22219  cpmatmcl  22221  mat2pmatf  22230  m2cpmf  22244  cpm2mf  22254  m2cpmfo  22258  m2cpminv  22262  decpmataa0  22270  pm2mpf  22300  pm2mpf1  22301  idpm2idmp  22303  pm2mpfo  22316  elcls2  22578  opnnei  22624  innei  22629  iscnp4  22767  cnpnei  22768  iscncl  22773  cnnei  22786  cnconst  22788  ordthauslem  22887  bwth  22914  1stccnp  22966  llyrest  22989  nllyrest  22990  kgenss  23047  xkoccn  23123  kqsat  23235  kqt0lem  23240  isr0  23241  fbssfi  23341  isfild  23362  filconn  23387  trfilss  23393  fgtr  23394  ufileu  23423  ufilen  23434  fmfnfmlem4  23461  fmfnfm  23462  hausflimi  23484  cnpflf2  23504  cnpflf  23505  cnpfcf  23545  cnextcn  23571  tsmsxplem1  23657  tsmsxp  23659  ustuqtop0  23745  ismeti  23831  isxmet2d  23833  elbl2ps  23895  elbl2  23896  xblpnfps  23901  xblpnf  23902  xbln0  23920  blin  23927  blssexps  23932  blssex  23933  blcls  24015  blsscls  24016  metrest  24033  metustbl  24075  psmetutop  24076  nmf2  24102  ngpi  24137  tngngp3  24173  nmdvr  24187  nmoi  24245  nmoix  24246  nmoleub  24248  nghmcn  24262  iccntr  24337  metdsle  24368  icoopnst  24455  iocopnst  24456  icccvx  24466  pi1xfr  24571  isclmi0  24614  iscvsi  24645  cphipval  24760  lmmbr  24775  lmmbr2  24776  iscfil3  24790  iscau2  24794  cfilres  24813  bcthlem1  24841  bcthlem4  24844  bcthlem5  24845  rrxmet  24925  ioombl  25082  iccvolcl  25084  ioovolcl  25087  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  ig1pcl  25693  ig1prsp  25695  aannenlem1  25841  taylplem1  25875  dvtaylp  25882  relogeftb  26093  logdivlt  26129  cxpexp  26176  rpcxpcl  26184  isppw2  26619  vmappw  26620  lgslem4  26803  lgscllem  26807  lgsneg1  26825  lgsne0  26838  nosepdm  27187  ssltdisj  27322  mulscutlem  27587  brbtwn2  28163  ax5seglem1  28186  ax5seglem2  28187  axcontlem4  28225  ewlkprop  28860  uspgr2wlkeq  28903  uhgrwkspthlem2  29011  clwlkclwwlkfo  29262  eupth2lem3lem7  29487  frgr3vlem2  29527  3cyclfrgrrn1  29538  4cycl2vnunb  29543  frgrncvvdeqlem8  29559  grpoidinvlem3  29759  isvciOLD  29833  nmcvcn  29948  ipval2lem2  29957  sspimsval  29991  isblo2  30036  nmoo0  30044  blocni  30058  isph  30075  hvadd4  30289  hiassdi  30344  ocsh  30536  chj4  30788  spansncol  30821  pjjsi  30953  hoscl  30998  hodcl  31000  hoadd4  31037  homco1  31054  homulass  31055  hoadddi  31056  hoadddir  31057  unoplin  31173  adjvalval  31190  hmoplin  31195  bralnfn  31201  brafnmul  31204  lnopmi  31253  lnopcoi  31256  hmops  31273  hmopm  31274  nmophmi  31284  lnfncnbd  31310  cnlnadjlem2  31321  adjlnop  31339  adjmul  31345  adjadd  31346  branmfn  31358  kbass5  31373  kbass6  31374  leop2  31377  leopadd  31385  leopmuli  31386  pjimai  31429  atcvatlem  31638  chirredlem2  31644  mdsymlem3  31658  mdsymlem5  31660  sumdmdii  31668  sumdmdlem  31671  cdj3lem2a  31689  cdj3lem2b  31690  cdj3lem3a  31692  cdj3i  31694  nn0difffzod  32016  xreceu  32088  cshwrnid  32125  toslublem  32142  tosglblem  32144  lmodvslmhm  32202  ogrpaddltbi  32236  archiabllem1b  32338  archiabllem2c  32341  archiabl  32344  slmdvsdir  32361  slmdvsass  32362  grplsm0l  32513  pidlnzb  32540  zarcls1  32849  pstmxmet  32877  ordtconnlem1  32904  hasheuni  33083  omsf  33295  ballotlemirc  33530  signswmnd  33568  bnj1204  34023  fineqvac  34097  fisshasheq  34104  revpfxsfxrev  34106  txpconn  34223  cvmscld  34264  satfbrsuc  34357  satfrnmapom  34361  satfun  34402  elmpps  34564  dfrdg2  34767  wsuclem  34797  segconeu  34983  linecom  35122  linethru  35125  lineintmo  35129  fnemeet2  35252  fnejoin2  35254  fvineqsneq  36293  lindsadd  36481  lindsdom  36482  lindsenlbs  36483  matunitlindflem1  36484  matunitlindflem2  36485  heicant  36523  mblfinlem1  36525  mblfinlem3  36527  ismblfin  36529  cnambfre  36536  itg2addnclem2  36540  ftc1anclem1  36561  ftc1anclem5  36565  ftc1anclem6  36566  ftc2nc  36570  areacirclem2  36577  areacirclem4  36579  areacirclem5  36580  areacirc  36581  fzmul  36609  subspopn  36620  isbndx  36650  isbnd2  36651  isbnd3  36652  ssbnd  36656  prdstotbnd  36662  heibor1  36678  rrnmet  36697  rngonegmn1l  36809  rngohomco  36842  rngoisocnv  36849  rngoisoco  36850  crngohomfo  36874  isidlc  36883  rngoidl  36892  prnc  36935  ispridlc  36938  cvrval2  38144  glbconxN  38249  hlrelat5N  38272  cvratlem  38292  cvrat2  38300  athgt  38327  3dim2  38339  llnn0  38387  lplnn0N  38418  lvoln0N  38462  snatpsubN  38621  paddasslem18  38708  pmod1i  38719  lhpexle2  38881  lhpexle3lem  38882  lhpexle3  38883  ldilcnv  38986  trlcnv  39036  trlnidatb  39048  cdleme32snaw  39306  cdleme32fvaw  39310  cdleme42ke  39356  cdlemeg46gf  39404  cdleme50trn12  39423  cdlemg1cex  39459  cdlemb3  39477  tgrpgrplem  39620  tgrpabl  39622  tendoplcl2  39649  tendo0pl  39662  tendoicl  39667  tendoipl  39668  cdlemkid3N  39804  tendoex  39846  erngdvlem4  39862  erngdvlem4-rN  39870  dib1dim  40036  dib1dim2  40039  dihglbcpreN  40171  dihmeetALTN  40198  dih1dimatlem  40200  dihatlat  40205  lcmineqlem1  40894  lcmineqlem3  40896  aks4d1p1  40941  aks4d1p7d1  40947  aks4d1p8  40952  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones8  40969  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones17  40979  sticksstones19  40981  metakunt29  41013  metakunt30  41014  metakunt31  41015  factwoffsmonot  41023  oddcomabszz  41683  acongtr  41717  rpnnen3lem  41770  islssfg  41812  lmhmfgsplit  41828  unxpwdom3  41837  hbtlem7  41867  iocmbl  41962  ss2iundf  42410  ismnu  43020  grumnudlem  43044  ismnushort  43060  nzss  43076  dvconstbi  43093  bccbc  43104  uzmptshftfval  43105  iccdifprioo  44229  climisp  44462  limsupresxr  44482  liminfresxr  44483  dvnmul  44659  volico  44699  volioore  44706  fourierdlem74  44896  fourierdlem75  44897  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0xp  45145  hspmbllem2  45343  smflimlem3  45489  smfsupmpt  45531  smfinflem  45533  smfinfmpt  45535  smflimsupmpt  45545  smfliminfmpt  45548  funressnbrafv2  45952  uniimaelsetpreimafv  46064  imasetpreimafvbijlemfv1  46071  imasetpreimafvbijlemfo  46073  sprsymrelfo  46165  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nn0mnd  46589  cntzsubrng  46746  rngqiprngimfo  46786  rnghmsubcsetclem2  46874  rhmsubcsetclem2  46920  rhmsubcrngclem2  46926  lcoss  47117  snlindsntorlem  47151  mreclat  47622  aacllem  47848