Theorem 3expa 1119

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3exp  1120  ad4ant123  1174  ad4ant124  1175  ad4ant134  1176  ad4ant234  1177  ad5ant123  1367  3anidm23  1424  mp3an2  1452  mpd3an3  1465  rgen3  3183  vtocl3  3512  spc3egv  3546  moi2  3663  sbc3ie  3807  2if2  4523  preq12bg  4797  ralxfrd2  5351  reuhypd  5358  otsndisj  5469  funcnvqp  6558  fvtp1g  7148  fntpb  7159  f1imass  7214  weisoeq  7305  f1ofveu  7356  f1ocnvfv3  7357  funeldmdif  7996  curry1f  8051  curry2f  8053  funsssuppss  8135  frrlem13  8243  tfrlem11  8322  oalimcl  8490  oeordsuc  8525  oelim2  8526  nneob  8587  nadd4  8629  mapxpen  9076  findcard  9093  enfii  9115  domtrfil  9121  domnsymfi  9129  phplem2  9134  php  9136  wemaplem3  9458  en2eqpr  9924  infxpabs  10128  infxp  10131  cfflb  10176  cfsmolem  10187  isf32lem12  10281  fin1a2lem9  10325  fin1a2s  10331  axcc3  10355  axdc3lem4  10370  zornn0g  10422  pwfseqlem4  10580  tskwun  10702  tskint  10703  tskxp  10705  tskmap  10706  gruf  10729  grutsk1  10739  addcanpi  10817  ltapi  10821  mul4  11309  add4  11362  2addsub  11402  addsubeq4  11403  muladd  11577  ltleadd  11628  receu  11790  p1le  11995  mulgt1  12012  lbinf  12104  zdiv  12594  fzind  12622  fnn0ind  12623  fzindd  12626  uzss  12806  zbtwnre  12891  qmulcl  12912  qreccl  12914  xrlttr  13086  xaddass  13196  xmulasslem3  13233  xadddilem  13241  xrsupsslem  13254  xrinfmsslem  13255  supxrunb1  13266  ioo0  13318  ico0  13339  ioc0  13340  icc0  13341  iooshf  13374  prunioo  13429  ioojoin  13431  elfz5  13465  elfz0fzfz0  13582  elfzonelfzo  13719  fzind2  13738  modaddb  13863  mulexpz  14059  expsub  14067  digit1  14194  facndiv  14245  faclbnd4lem4  14253  faclbnd4  14254  faclbnd5  14255  bccmpl  14266  bcval5  14275  bcpasc  14278  hashunx  14343  hashunsnggt  14351  hashdmpropge2  14440  ccatrn  14547  swrdspsleq  14623  swrdccat2  14627  ccatpfx  14658  pfxccat1  14659  swrdswrd  14662  cshf1  14767  crim  15072  absmax  15287  ello12r  15474  elo12r  15485  climshftlem  15531  2sumeq2dv  15662  hash2iun  15781  expcnv  15824  2cprodeq2dv  15885  rpnnen2lem7  16182  dvdsval3  16220  dvdsnegb  16237  muldvds1  16244  muldvds2  16245  dvdscmul  16246  dvdsmulc  16247  dvdsmulcr  16249  dvds2ln  16253  divalgb  16368  ndvdssub  16373  gcddiv  16515  lcmfval  16585  lcmfcl  16592  dvdslcmf  16595  rpexp1i  16688  phiprmpw  16741  hashgcdeq  16755  pythagtriplem1  16782  pockthg  16872  infpnlem1  16876  4sqlem3  16916  0ramcl  16989  firest  17390  imasaddfnlem  17487  imasleval  17500  mrerintcl  17554  iscatd  17634  fullestrcsetc  18112  fullsetcestrc  18127  clatleglb  18479  mreclatBAD  18524  pslem  18533  mndind  18791  grplmulf1o  18984  grplactcnv  19014  mulgnn0subcl  19058  mulgsubcl  19059  mulgdir  19077  issubg2  19112  issubgrpd2  19113  nmzsubg  19135  eqgen  19151  cycsubm  19172  cycsubgcl  19176  cycsubgss  19177  ghmmulg  19198  ghmf1  19216  kerf1ghm  19217  conjghm  19219  symgpssefmnd  19366  gsmsymgreqlem2  19401  symgfixfo  19409  odeq  19520  odval2  19521  odf1  19532  dfod2  19534  gexdvds  19554  gexdvds2  19555  gexcl2  19559  gexdvds3  19560  sylow2blem2  19591  efgsp1  19707  efgrelexlemb  19720  cmnbascntr  19775  mulgmhm  19797  mulgghm  19798  iscyggen2  19851  iscyg3  19856  ablsimpgfindlem1  20079  ogrpaddltbi  20109  srglmhm  20197  srgrmhm  20198  ringlghm  20288  ringrghm  20289  gsumdixp  20293  dvdsrcl2  20341  crngunit  20353  cntzsubrng  20539  subrgugrp  20563  cntzsubr  20578  rnghmsubcsetclem2  20604  rhmsubcsetclem2  20633  rhmsubcrngclem2  20639  sdrgacs  20773  lmodvsdir  20876  lmodvsass  20877  lmodvsghm  20913  lsssubg  20947  lss1d  20953  islbs2  21148  lidlsubg  21217  lidlsubcl  21218  rngqiprngimfo  21295  lpigen  21329  xrsdsreval  21405  expghm  21469  mulgghm2  21470  ip0r  21631  obs2ss  21723  islindf3  21820  scmatscm  22492  scmataddcl  22495  scmatsubcl  22496  scmatfo  22509  matunit  22657  cpmatelimp  22691  cpmatelimp2  22693  cpmatinvcl  22696  cpmatmcl  22698  mat2pmatf  22707  m2cpmf  22721  cpm2mf  22731  m2cpmfo  22735  m2cpminv  22739  decpmataa0  22747  pm2mpf  22777  pm2mpf1  22778  idpm2idmp  22780  pm2mpfo  22793  elcls2  23053  opnnei  23099  innei  23104  iscnp4  23242  cnpnei  23243  iscncl  23248  cnnei  23261  cnconst  23263  ordthauslem  23362  bwth  23389  1stccnp  23441  llyrest  23464  nllyrest  23465  kgenss  23522  xkoccn  23598  kqsat  23710  kqt0lem  23715  isr0  23716  fbssfi  23816  isfild  23837  filconn  23862  trfilss  23868  fgtr  23869  ufileu  23898  ufilen  23909  fmfnfmlem4  23936  fmfnfm  23937  hausflimi  23959  cnpflf2  23979  cnpflf  23980  cnpfcf  24020  cnextcn  24046  tsmsxplem1  24132  tsmsxp  24134  ustuqtop0  24219  ismeti  24304  isxmet2d  24306  elbl2ps  24368  elbl2  24369  xblpnfps  24374  xblpnf  24375  xbln0  24393  blin  24400  blssexps  24405  blssex  24406  blcls  24485  blsscls  24486  metrest  24503  metustbl  24545  psmetutop  24546  nmf2  24572  ngpi  24607  tngngp3  24635  nmdvr  24649  nmoi  24707  nmoix  24708  nmoleub  24710  nghmcn  24724  iccntr  24801  metdsle  24832  icoopnst  24920  iocopnst  24921  icccvx  24931  pi1xfr  25036  isclmi0  25079  iscvsi  25110  cphipval  25224  lmmbr  25239  lmmbr2  25240  iscfil3  25254  iscau2  25258  cfilres  25277  bcthlem1  25305  bcthlem4  25308  bcthlem5  25309  rrxmet  25389  ioombl  25546  iccvolcl  25548  ioovolcl  25551  mbfi1fseqlem3  25698  mbfi1fseqlem4  25699  mbfi1fseqlem5  25700  ig1pcl  26158  ig1prsp  26160  aannenlem1  26309  taylplem1  26343  dvtaylp  26351  relogeftb  26565  logdivlt  26602  cxpexp  26649  rpcxpcl  26657  isppw2  27096  vmappw  27097  lgslem4  27281  lgscllem  27285  lgsneg1  27303  lgsne0  27316  nosepdm  27666  sltsdisj  27813  mulcutlem  28141  ltonold  28271  zsoring  28419  bdayfinbndlem1  28477  z12bdaylem  28494  brbtwn2  28992  ax5seglem1  29015  ax5seglem2  29016  axcontlem4  29054  ewlkprop  29691  uspgr2wlkeq  29733  uhgrwkspthlem2  29841  clwlkclwwlkfo  30098  eupth2lem3lem7  30323  frgr3vlem2  30363  3cyclfrgrrn1  30374  4cycl2vnunb  30379  frgrncvvdeqlem8  30395  grpoidinvlem3  30596  isvciOLD  30670  nmcvcn  30785  ipval2lem2  30794  sspimsval  30828  isblo2  30873  nmoo0  30881  blocni  30895  isph  30912  hvadd4  31126  hiassdi  31181  ocsh  31373  chj4  31625  spansncol  31658  pjjsi  31790  hoscl  31835  hodcl  31837  hoadd4  31874  homco1  31891  homulass  31892  hoadddi  31893  hoadddir  31894  unoplin  32010  adjvalval  32027  hmoplin  32032  bralnfn  32038  brafnmul  32041  lnopmi  32090  lnopcoi  32093  hmops  32110  hmopm  32111  nmophmi  32121  lnfncnbd  32147  cnlnadjlem2  32158  adjlnop  32176  adjmul  32182  adjadd  32183  branmfn  32195  kbass5  32210  kbass6  32211  leop2  32214  leopadd  32222  leopmuli  32223  pjimai  32266  atcvatlem  32475  chirredlem2  32481  mdsymlem3  32495  mdsymlem5  32497  sumdmdii  32505  sumdmdlem  32508  cdj3lem2a  32526  cdj3lem2b  32527  cdj3lem3a  32529  cdj3i  32531  nn0difffzod  32896  xreceu  33000  cshwrnid  33040  toslublem  33051  tosglblem  33053  lmodvslmhm  33130  archiabllem1b  33272  archiabllem2c  33275  archiabl  33278  slmdvsdir  33296  slmdvsass  33297  grplsm0l  33482  pidlnzb  33501  rprmndvdsru  33608  mplvrpmmhm  33709  mplvrpmrhm  33710  zarcls1  34033  pstmxmet  34061  ordtconnlem1  34088  hasheuni  34249  omsf  34460  ballotlemirc  34696  signswmnd  34721  bnj1204  35174  fineqvac  35280  fisshasheq  35317  revpfxsfxrev  35318  txpconn  35434  cvmscld  35475  satfbrsuc  35568  satfrnmapom  35572  satfun  35613  elmpps  35775  dfrdg2  35995  wsuclem  36025  segconeu  36213  linecom  36352  linethru  36355  lineintmo  36359  fnemeet2  36569  fnejoin2  36571  fvineqsneq  37746  lindsadd  37952  lindsdom  37953  lindsenlbs  37954  matunitlindflem1  37955  matunitlindflem2  37956  heicant  37994  mblfinlem1  37996  mblfinlem3  37998  ismblfin  38000  cnambfre  38007  itg2addnclem2  38011  ftc1anclem1  38032  ftc1anclem5  38036  ftc1anclem6  38037  ftc2nc  38041  areacirclem2  38048  areacirclem4  38050  areacirclem5  38051  areacirc  38052  fzmul  38080  subspopn  38091  isbndx  38121  isbnd2  38122  isbnd3  38123  ssbnd  38127  prdstotbnd  38133  heibor1  38149  rrnmet  38168  rngonegmn1l  38280  rngohomco  38313  rngoisocnv  38320  rngoisoco  38321  crngohomfo  38345  isidlc  38354  rngoidl  38363  prnc  38406  ispridlc  38409  cvrval2  39738  glbconxN  39842  hlrelat5N  39865  cvratlem  39885  cvrat2  39893  athgt  39920  3dim2  39932  llnn0  39980  lplnn0N  40011  lvoln0N  40055  snatpsubN  40214  paddasslem18  40301  pmod1i  40312  lhpexle2  40474  lhpexle3lem  40475  lhpexle3  40476  ldilcnv  40579  trlcnv  40629  trlnidatb  40641  cdleme32snaw  40899  cdleme32fvaw  40903  cdleme42ke  40949  cdlemeg46gf  40997  cdleme50trn12  41016  cdlemg1cex  41052  cdlemb3  41070  tgrpgrplem  41213  tgrpabl  41215  tendoplcl2  41242  tendo0pl  41255  tendoicl  41260  tendoipl  41261  cdlemkid3N  41397  tendoex  41439  erngdvlem4  41455  erngdvlem4-rN  41463  dib1dim  41629  dib1dim2  41632  dihglbcpreN  41764  dihmeetALTN  41791  dih1dimatlem  41793  dihatlat  41798  lcmineqlem1  42486  lcmineqlem3  42488  aks4d1p1  42533  aks4d1p7d1  42539  aks4d1p8  42544  sticksstones1  42603  sticksstones2  42604  sticksstones3  42605  sticksstones8  42610  sticksstones10  42612  sticksstones11  42613  sticksstones12a  42614  sticksstones12  42615  sticksstones17  42620  sticksstones19  42622  oddcomabszz  43394  acongtr  43428  rpnnen3lem  43481  islssfg  43520  lmhmfgsplit  43536  unxpwdom3  43545  hbtlem7  43575  iocmbl  43663  ss2iundf  44108  ismnu  44710  grumnudlem  44734  ismnushort  44750  nzss  44766  dvconstbi  44783  bccbc  44794  uzmptshftfval  44795  iccdifprioo  45968  climisp  46196  limsupresxr  46216  liminfresxr  46217  dvnmul  46393  volico  46433  volioore  46440  fourierdlem74  46630  fourierdlem75  46631  sge0iunmptlemfi  46863  sge0iunmptlemre  46865  sge0iunmpt  46868  sge0xp  46879  hspmbllem2  47077  smflimlem3  47223  smfsupmpt  47265  smfinflem  47267  smfinfmpt  47269  smflimsupmpt  47279  smfliminfmpt  47282  funressnbrafv2  47708  uniimaelsetpreimafv  47872  imasetpreimafvbijlemfv1  47879  imasetpreimafvbijlemfo  47881  sprsymrelfo  47973  nnsum4primesodd  48288  nnsum4primesoddALTV  48289  grtrissvtx  48436  gricgrlic  48510  nn0mnd  48671  lcoss  48928  snlindsntorlem  48962  mreclat  49488  aacllem  50292