Theorem 3expa 1136

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-3an 1105

This theorem is referenced by:  3exp  1137  ad4ant123  1191  ad4ant124  1192  ad4ant134  1193  ad4ant234  1194  ad5ant123  1387  ad5ant124  1388  ad5ant125  1390  3anidm23  1448  mp3an2  1478  mpd3an3  1491  rgen3  3210  vtocl3  3532  spc3egv  3562  moi2  3679  sbc3ie  3821  2if2  4543  preq12bg  4818  ralxfrd2  5383  reuhypd  5390  otsndisj  5502  funcnvqp  6600  fvtp1g  7196  fntpb  7207  f1imass  7262  weisoeq  7353  f1ofveu  7404  f1ocnvfv3  7405  funeldmdif  8041  curry1f  8097  curry2f  8099  funsssuppss  8182  frrlem13  8291  tfrlem11  8371  oalimcl  8541  oeordsuc  8576  oelim2  8577  nneob  8638  nadd4  8681  mapxpen  9127  findcard  9144  enfii  9166  domtrfil  9172  domnsymfi  9180  phplem2  9185  php  9187  wemaplem3  9506  en2eqpr  9987  infxpabs  10190  infxp  10193  cfflb  10238  cfsmolem  10249  isf32lem12  10343  fin1a2lem9  10387  fin1a2s  10393  axcc3  10417  axdc3lem4  10432  zornn0g  10484  pwfseqlem4  10642  tskwun  10764  tskint  10765  tskxp  10767  tskmap  10768  gruf  10791  grutsk1  10801  addcanpi  10879  ltapi  10883  mul4  11373  add4  11426  2addsub  11466  addsubeq4  11467  muladd  11641  ltleadd  11692  receu  11854  p1le  12055  mulgt1  12071  lbinf  12163  zdiv  12661  fzind  12689  fnn0ind  12690  fzindd  12693  uzss  12880  zbtwnre  12965  qmulcl  12986  qreccl  12988  xrlttr  13160  xaddass  13270  xmulasslem3  13307  xadddilem  13315  xrsupsslem  13328  xrinfmsslem  13329  supxrunb1  13340  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  iooshf  13448  prunioo  13503  ioojoin  13505  elfz5  13539  elfz0fzfz0  13657  elfzonelfzo  13794  fzind2  13813  modaddb  13938  mulexpz  14134  expsub  14142  digit1  14269  facndiv  14320  faclbnd4lem4  14328  faclbnd4  14329  faclbnd5  14330  bccmpl  14341  bcval5  14350  bcpasc  14353  hashunx  14418  hashunsnggt  14426  hashdmpropge2  14516  ccatrn  14623  swrdspsleq  14699  swrdccat2  14703  ccatpfx  14734  pfxccat1  14735  swrdswrd  14738  cshf1  14843  crim  15162  absmax  15377  ello12r  15564  elo12r  15575  climshftlem  15621  2sumeq2dv  15752  hash2iun  15871  expcnv  15914  2cprodeq2dv  15975  rpnnen2lem7  16271  dvdsval3  16309  dvdsnegb  16326  muldvds1  16333  muldvds2  16334  dvdscmul  16335  dvdsmulc  16336  dvdsmulcr  16338  dvds2ln  16342  divalgb  16457  ndvdssub  16462  gcddiv  16604  lcmfval  16674  lcmfcl  16681  dvdslcmf  16684  rpexp1i  16777  phiprmpw  16830  hashgcdeq  16844  pythagtriplem1  16871  pockthg  16961  infpnlem1  16965  4sqlem3  17005  0ramcl  17078  firest  17480  imasaddfnlem  17577  imasleval  17590  mrerintcl  17644  iscatd  17724  fullestrcsetc  18202  fullsetcestrc  18217  clatleglb  18569  mreclatBAD  18614  pslem  18623  mndind  18882  grplmulf1o  19074  grplactcnv  19104  mulgnn0subcl  19148  mulgsubcl  19149  mulgdir  19167  issubg2  19203  issubgrpd2  19204  nmzsubg  19226  eqgen  19244  cycsubm  19268  cycsubgcl  19272  cycsubgss  19273  ghmmulg  19293  ghmf1  19311  kerf1ghm  19312  conjghm  19314  symgpssefmnd  19461  gsmsymgreqlem2  19496  symgfixfo  19504  odeq  19615  odval2  19616  odf1  19627  dfod2  19629  gexdvds  19649  gexdvds2  19650  gexcl2  19654  gexdvds3  19655  sylow2blem2  19686  efgsp1  19802  efgrelexlemb  19815  cmnbascntr  19870  mulgmhm  19892  mulgghm  19893  iscyggen2  19946  iscyg3  19951  ablsimpgfindlem1  20174  ogrpaddltbi  20204  srglmhm  20298  srgrmhm  20299  ringlghm  20391  ringrghm  20392  gsumdixp  20396  dvdsrcl2  20444  crngunit  20456  cntzsubrng  20666  subrgugrp  20690  cntzsubr  20705  rnghmsubcsetclem2  20731  rhmsubcsetclem2  20760  rhmsubcrngclem2  20766  sdrgacs  20904  lmodvsdir  21007  lmodvsass  21008  lmodvsghm  21044  lsssubg  21078  lss1d  21084  islbs2  21278  lidlsubg  21348  lidlsubcl  21349  rngqiprngimfo  21441  lpigen  21503  xrsdsreval  21562  expghm  21625  mulgghm2  21626  ip0r  21787  obs2ss  21879  islindf3  21976  scmatscm  22670  scmataddcl  22673  scmatsubcl  22674  scmatfo  22687  matunit  22835  cpmatelimp  22869  cpmatelimp2  22871  cpmatinvcl  22874  cpmatmcl  22876  mat2pmatf  22885  m2cpmf  22899  cpm2mf  22909  m2cpmfo  22913  m2cpminv  22917  decpmataa0  22925  pm2mpf  22955  pm2mpf1  22956  idpm2idmp  22958  pm2mpfo  22971  elcls2  23231  opnnei  23277  innei  23282  iscnp4  23420  cnpnei  23421  iscncl  23426  cnnei  23439  cnconst  23441  ordthauslem  23540  bwth  23567  1stccnp  23619  llyrest  23642  nllyrest  23643  kgenss  23700  xkoccn  23776  kqsat  23888  kqt0lem  23893  isr0  23894  fbssfi  23994  isfild  24015  filconn  24040  trfilss  24046  fgtr  24047  ufileu  24076  ufilen  24087  fmfnfmlem4  24114  fmfnfm  24115  hausflimi  24137  cnpflf2  24157  cnpflf  24158  cnpfcf  24198  cnextcn  24224  tsmsxplem1  24310  tsmsxp  24312  ustuqtop0  24397  ismeti  24482  isxmet2d  24484  elbl2ps  24546  elbl2  24547  xblpnfps  24552  xblpnf  24553  xbln0  24571  blin  24578  blssexps  24583  blssex  24584  blcls  24663  blsscls  24664  metrest  24681  metustbl  24723  psmetutop  24724  nmf2  24750  ngpi  24785  tngngp3  24813  nmdvr  24827  nmoi  24885  nmoix  24886  nmoleub  24888  nghmcn  24902  iccntr  24979  metdsle  25010  icoopnst  25098  iocopnst  25099  icccvx  25109  pi1xfr  25214  isclmi0  25257  iscvsi  25288  cphipval  25402  lmmbr  25417  lmmbr2  25418  iscfil3  25432  iscau2  25436  cfilres  25455  bcthlem1  25483  bcthlem4  25486  bcthlem5  25487  rrxmet  25567  ioombl  25724  iccvolcl  25726  ioovolcl  25729  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  ig1pcl  26336  ig1prsp  26338  aannenlem1  26491  taylplem1  26526  dvtaylp  26533  relogeftb  26749  logdivlt  26786  cxpexp  26833  rpcxpcl  26841  isppw2  27279  vmappw  27280  lgslem4  27464  lgscllem  27468  lgsneg1  27486  lgsne0  27499  nosepdm  27848  sltsdisj  27996  mulcutlem  28324  ltonold  28454  zsoring  28602  bdayfinbndlem1  28660  z12bdaylem  28677  brbtwn2  29255  ax5seglem1  29278  ax5seglem2  29279  axcontlem4  29317  ewlkprop  29953  uspgr2wlkeq  29995  uhgrwkspthlem2  30103  clwlkclwwlkfo  30360  eupth2lem3lem7  30585  frgr3vlem2  30625  3cyclfrgrrn1  30636  4cycl2vnunb  30641  frgrncvvdeqlem8  30657  grpoidinvlem3  30858  isvciOLD  30932  nmcvcn  31047  ipval2lem2  31056  sspimsval  31090  isblo2  31135  nmoo0  31143  blocni  31157  isph  31174  hvadd4  31388  hiassdi  31443  ocsh  31635  chj4  31887  spansncol  31920  pjjsi  32052  hoscl  32097  hodcl  32099  hoadd4  32136  homco1  32153  homulass  32154  hoadddi  32155  hoadddir  32156  unoplin  32272  adjvalval  32289  hmoplin  32294  bralnfn  32300  brafnmul  32303  lnopmi  32352  lnopcoi  32355  hmops  32372  hmopm  32373  nmophmi  32383  lnfncnbd  32409  cnlnadjlem2  32420  adjlnop  32438  adjmul  32444  adjadd  32445  branmfn  32457  kbass5  32472  kbass6  32473  leop2  32476  leopadd  32484  leopmuli  32485  pjimai  32528  atcvatlem  32737  chirredlem2  32743  mdsymlem3  32757  mdsymlem5  32759  sumdmdii  32767  sumdmdlem  32770  cdj3lem2a  32788  cdj3lem2b  32789  cdj3lem3a  32791  cdj3i  32793  nn0difffzod  33149  xreceu  33241  cshwrnid  33281  toslublem  33292  tosglblem  33294  lmodvslmhm  33370  archiabllem1b  33512  archiabllem2c  33515  archiabl  33518  slmdvsdir  33536  slmdvsass  33537  grplsm0l  33712  pidlnzb  33730  rprmndvdsru  33819  mplvrpmmhm  33936  mplvrpmrhm  33937  zarcls1  34259  pstmxmet  34287  ordtconnlem1  34314  hasheuni  34475  omsf  34686  ballotlemirc  34922  signswmnd  34944  bnj1204  35400  fineqvac  35529  fisshasheq  35606  revpfxsfxrev  35607  txpconn  35724  cvmscld  35765  satfbrsuc  35858  satfrnmapom  35862  satfun  35903  elmpps  36065  dfrdg2  36285  wsuclem  36315  segconeu  36503  linecom  36642  linethru  36645  lineintmo  36649  fnemeet2  36898  fnejoin2  36900  fvineqsneq  38078  lindsadd  38284  lindsdom  38285  lindsenlbs  38286  matunitlindflem1  38287  matunitlindflem2  38288  heicant  38326  mblfinlem1  38328  mblfinlem3  38330  ismblfin  38332  cnambfre  38339  itg2addnclem2  38343  ftc1anclem1  38364  ftc1anclem5  38368  ftc1anclem6  38369  ftc2nc  38373  areacirclem2  38380  areacirclem4  38382  areacirclem5  38383  areacirc  38384  fzmul  38412  subspopn  38423  isbndx  38453  isbnd2  38454  isbnd3  38455  ssbnd  38459  prdstotbnd  38465  heibor1  38481  rrnmet  38500  rngonegmn1l  38612  rngohomco  38645  rngoisocnv  38652  rngoisoco  38653  crngohomfo  38677  isidlc  38686  rngoidl  38695  prnc  38738  ispridlc  38741  cvrval2  40068  glbconxN  40172  hlrelat5N  40195  cvratlem  40215  cvrat2  40223  athgt  40250  3dim2  40262  llnn0  40310  lplnn0N  40341  lvoln0N  40385  snatpsubN  40544  paddasslem18  40631  pmod1i  40642  lhpexle2  40804  lhpexle3lem  40805  lhpexle3  40806  ldilcnv  40909  trlcnv  40959  trlnidatb  40971  cdleme32snaw  41229  cdleme32fvaw  41233  cdleme42ke  41279  cdlemeg46gf  41327  cdleme50trn12  41346  cdlemg1cex  41382  cdlemb3  41400  tgrpgrplem  41543  tgrpabl  41545  tendoplcl2  41572  tendo0pl  41585  tendoicl  41590  tendoipl  41591  cdlemkid3N  41727  tendoex  41769  erngdvlem4  41785  erngdvlem4-rN  41793  dib1dim  41959  dib1dim2  41962  dihglbcpreN  42094  dihmeetALTN  42121  dih1dimatlem  42123  dihatlat  42128  lcmineqlem1  42816  lcmineqlem3  42818  aks4d1p1  42863  aks4d1p7d1  42869  aks4d1p8  42874  sticksstones1  42933  sticksstones2  42934  sticksstones3  42935  sticksstones8  42940  sticksstones10  42942  sticksstones11  42943  sticksstones12a  42944  sticksstones12  42945  sticksstones17  42950  sticksstones19  42952  oddcomabszz  43691  acongtr  43725  rpnnen3lem  43778  islssfg  43817  lmhmfgsplit  43833  unxpwdom3  43842  hbtlem7  43872  iocmbl  43960  ss2iundf  44405  ismnu  44991  grumnudlem  45015  ismnushort  45031  nzss  45047  dvconstbi  45064  bccbc  45075  uzmptshftfval  45076  iccdifprioo  46252  climisp  46480  limsupresxr  46500  liminfresxr  46501  dvnmul  46677  volico  46717  volioore  46724  fourierdlem74  46914  fourierdlem75  46915  sge0iunmptlemfi  47147  sge0iunmptlemre  47149  sge0iunmpt  47152  sge0xp  47163  hspmbllem2  47361  smflimlem3  47507  smfsupmpt  47549  smfinflem  47551  smfinfmpt  47553  smflimsupmpt  47563  smfliminfmpt  47566  funressnbrafv2  48001  uniimaelsetpreimafv  48165  imasetpreimafvbijlemfv1  48172  imasetpreimafvbijlemfo  48174  sprsymrelfo  48266  nnsum4primesodd  48581  nnsum4primesoddALTV  48582  grtrissvtx  48729  gricgrlic  48803  nn0mnd  48964  lcoss  49236  snlindsntorlem  49270  mreclat  49795  aacllem  50641