MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expa Structured version   Visualization version   GIF version

Theorem 3expa 1115
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1116 and pm3.2an3 1337 by Wolf Lammen, 22-Jun-2022.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expa (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa
StepHypRef Expression
1 df-3an 1086 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbir 238 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 1086
This theorem is referenced by:  3exp  1116  ad4ant123  1169  ad4ant124  1170  ad4ant134  1171  ad4ant234  1172  ad5ant123  1361  3anidm23  1418  mp3an2  1446  mpd3an3  1459  rgen3  3172  vtocl3  3514  spc3egv  3555  moi2  3658  sbc3ie  3801  2if2  4481  preq12bg  4747  ralxfrd2  5281  reuhypd  5288  otsndisj  5377  funcnvqp  6392  fvtp1g  6941  fntpb  6953  f1imass  7004  weisoeq  7091  f1ofveu  7134  f1ocnvfv3  7135  funeldmdif  7733  curry1f  7788  curry2f  7790  funsssuppss  7843  tfrlem11  8011  oalimcl  8173  oeordsuc  8207  oelim2  8208  nneob  8266  mapxpen  8671  findcard  8745  wemaplem3  9000  en2eqpr  9422  infxpabs  9627  infxp  9630  cfflb  9674  cfsmolem  9685  isf32lem12  9779  fin1a2lem9  9823  fin1a2s  9829  axcc3  9853  axdc3lem4  9868  zornn0g  9920  pwfseqlem4  10077  tskwun  10199  tskint  10200  tskxp  10202  tskmap  10203  gruf  10226  grutsk1  10236  addcanpi  10314  ltapi  10318  mul4  10801  add4  10853  2addsub  10893  addsubeq4  10894  muladd  11065  ltleadd  11116  receu  11278  p1le  11478  lbinf  11585  zdiv  12044  fzind  12072  fnn0ind  12073  uzss  12257  zbtwnre  12338  qmulcl  12358  qreccl  12360  xrlttr  12525  xaddass  12634  xmulasslem3  12671  xadddilem  12679  xrsupsslem  12692  xrinfmsslem  12693  supxrunb1  12704  ioo0  12755  ico0  12776  ioc0  12777  icc0  12778  iooshf  12808  prunioo  12863  ioojoin  12865  elfz5  12898  elfz0fzfz0  13011  elfzonelfzo  13138  fzind2  13154  mulexpz  13469  expsub  13477  digit1  13598  facndiv  13648  faclbnd4lem4  13656  faclbnd4  13657  faclbnd5  13658  bccmpl  13669  bcval5  13678  bcpasc  13681  hashunx  13747  hashunsnggt  13755  hashdmpropge2  13841  ccatrn  13938  swrdspsleq  14022  swrdccat2  14026  ccatpfx  14058  pfxccat1  14059  swrdswrd  14062  cshf1  14167  crim  14469  absmax  14684  ello12r  14869  elo12r  14880  climshftlem  14926  2sumeq2dv  15057  hash2iun  15173  expcnv  15214  2cprodeq2dv  15274  rpnnen2lem7  15568  dvdsval3  15606  dvdsnegb  15622  muldvds1  15629  muldvds2  15630  dvdscmul  15631  dvdsmulc  15632  dvdsmulcr  15634  dvds2ln  15637  divalgb  15748  ndvdssub  15753  gcddiv  15892  lcmfval  15958  lcmfcl  15965  dvdslcmf  15968  rpexp1i  16058  phiprmpw  16106  hashgcdeq  16119  pythagtriplem1  16146  pockthg  16235  infpnlem1  16239  4sqlem3  16279  0ramcl  16352  firest  16701  imasaddfnlem  16796  imasleval  16809  mrerintcl  16863  iscatd  16939  fullestrcsetc  17396  fullsetcestrc  17411  clatleglb  17731  mreclatBAD  17792  pslem  17811  mndind  17987  grplmulf1o  18168  grplactcnv  18197  mulgnn0subcl  18236  mulgsubcl  18237  mulgdir  18254  issubg2  18289  issubgrpd2  18290  nmzsubg  18312  eqgen  18328  cycsubm  18340  cycsubgcl  18344  cycsubgss  18345  ghmmulg  18365  conjghm  18384  symgpssefmnd  18519  gsmsymgreqlem2  18554  symgfixfo  18562  odeq  18673  odval2  18674  odf1  18684  dfod2  18686  gexdvds  18704  gexdvds2  18705  gexcl2  18709  gexdvds3  18710  sylow2blem2  18741  efgsp1  18858  efgrelexlemb  18871  mulgmhm  18944  mulgghm  18945  iscyggen2  18996  iscyg3  19001  ablsimpgfindlem1  19225  srglmhm  19281  srgrmhm  19282  ringlghm  19353  ringrghm  19354  gsumdixp  19358  dvdsrcl2  19399  crngunit  19411  kerf1ghm  19494  subrgugrp  19550  cntzsubr  19564  sdrgacs  19576  lmodvsdir  19654  lmodvsass  19655  lmodvsghm  19691  lsssubg  19725  lss1d  19731  islbs2  19922  lidlsubg  19984  lidlsubcl  19985  quscrng  20009  lpigen  20025  xrsdsreval  20139  expghm  20192  mulgghm2  20193  ip0r  20329  obs2ss  20421  islindf3  20518  scmatscm  21121  scmataddcl  21124  scmatsubcl  21125  scmatfo  21138  matunit  21286  cpmatelimp  21320  cpmatelimp2  21322  cpmatinvcl  21325  cpmatmcl  21327  mat2pmatf  21336  m2cpmf  21350  cpm2mf  21360  m2cpmfo  21364  m2cpminv  21368  decpmataa0  21376  pm2mpf  21406  pm2mpf1  21407  idpm2idmp  21409  pm2mpfo  21422  elcls2  21682  opnnei  21728  innei  21733  iscnp4  21871  cnpnei  21872  iscncl  21877  cnnei  21890  cnconst  21892  ordthauslem  21991  bwth  22018  1stccnp  22070  llyrest  22093  nllyrest  22094  kgenss  22151  xkoccn  22227  kqsat  22339  kqt0lem  22344  isr0  22345  fbssfi  22445  isfild  22466  filconn  22491  trfilss  22497  fgtr  22498  ufileu  22527  ufilen  22538  fmfnfmlem4  22565  fmfnfm  22566  hausflimi  22588  cnpflf2  22608  cnpflf  22609  cnpfcf  22649  cnextcn  22675  tsmsxplem1  22761  tsmsxp  22763  ustuqtop0  22849  ismeti  22935  isxmet2d  22937  elbl2ps  22999  elbl2  23000  xblpnfps  23005  xblpnf  23006  xbln0  23024  blin  23031  blssexps  23036  blssex  23037  blcls  23116  blsscls  23117  metrest  23134  metustbl  23176  psmetutop  23177  nmf2  23202  ngpi  23237  tngngp3  23265  nmdvr  23279  nmoi  23337  nmoix  23338  nmoleub  23340  nghmcn  23354  iccntr  23429  metdsle  23460  icoopnst  23547  iocopnst  23548  icccvx  23558  pi1xfr  23663  isclmi0  23706  iscvsi  23737  cphipval  23850  lmmbr  23865  lmmbr2  23866  iscfil3  23880  iscau2  23884  cfilres  23903  bcthlem1  23931  bcthlem4  23934  bcthlem5  23935  rrxmet  24015  ioombl  24172  iccvolcl  24174  ioovolcl  24177  mbfi1fseqlem3  24324  mbfi1fseqlem4  24325  mbfi1fseqlem5  24326  ig1pcl  24779  ig1prsp  24781  aannenlem1  24927  taylplem1  24961  dvtaylp  24968  relogeftb  25179  logdivlt  25215  cxpexp  25262  rpcxpcl  25270  isppw2  25703  vmappw  25704  lgslem4  25887  lgscllem  25891  lgsneg1  25909  lgsne0  25922  brbtwn2  26702  ax5seglem1  26725  ax5seglem2  26726  axcontlem4  26764  ewlkprop  27396  uspgr2wlkeq  27438  uhgrwkspthlem2  27546  clwlkclwwlkfo  27797  eupth2lem3lem7  28022  frgr3vlem2  28062  3cyclfrgrrn1  28073  4cycl2vnunb  28078  frgrncvvdeqlem8  28094  grpoidinvlem3  28292  isvciOLD  28366  nmcvcn  28481  ipval2lem2  28490  sspimsval  28524  isblo2  28569  nmoo0  28577  blocni  28591  isph  28608  hvadd4  28822  hiassdi  28877  ocsh  29069  chj4  29321  spansncol  29354  pjjsi  29486  hoscl  29531  hodcl  29533  hoadd4  29570  homco1  29587  homulass  29588  hoadddi  29589  hoadddir  29590  unoplin  29706  adjvalval  29723  hmoplin  29728  bralnfn  29734  brafnmul  29737  lnopmi  29786  lnopcoi  29789  hmops  29806  hmopm  29807  nmophmi  29817  lnfncnbd  29843  cnlnadjlem2  29854  adjlnop  29872  adjmul  29878  adjadd  29879  branmfn  29891  kbass5  29906  kbass6  29907  leop2  29910  leopadd  29918  leopmuli  29919  pjimai  29962  atcvatlem  30171  chirredlem2  30177  mdsymlem3  30191  mdsymlem5  30193  sumdmdii  30201  sumdmdlem  30204  cdj3lem2a  30222  cdj3lem2b  30223  cdj3lem3a  30225  cdj3i  30227  xreceu  30627  cshwrnid  30664  toslublem  30683  tosglblem  30685  lmodvslmhm  30738  ogrpaddltbi  30772  archiabllem1b  30874  archiabllem2c  30877  archiabl  30880  slmdvsdir  30897  slmdvsass  30898  zarcls1  31222  pstmxmet  31248  ordtconnlem1  31275  hasheuni  31452  omsf  31662  ballotlemirc  31897  signswmnd  31935  bnj1204  32392  fisshasheq  32460  revpfxsfxrev  32470  txpconn  32587  cvmscld  32628  satfbrsuc  32721  satfrnmapom  32725  satfun  32766  elmpps  32928  dfrdg2  33148  wsuclem  33220  frrlem13  33243  nosepdm  33296  segconeu  33580  linecom  33719  linethru  33722  lineintmo  33726  fnemeet2  33823  fnejoin2  33825  fvineqsneq  34824  lindsadd  35043  lindsdom  35044  lindsenlbs  35045  matunitlindflem1  35046  matunitlindflem2  35047  heicant  35085  mblfinlem1  35087  mblfinlem3  35089  ismblfin  35091  cnambfre  35098  itg2addnclem2  35102  ftc1anclem1  35123  ftc1anclem5  35127  ftc1anclem6  35128  ftc2nc  35132  areacirclem2  35139  areacirclem4  35141  areacirclem5  35142  areacirc  35143  fzmul  35172  subspopn  35183  isbndx  35213  isbnd2  35214  isbnd3  35215  ssbnd  35219  prdstotbnd  35225  heibor1  35241  rrnmet  35260  rngonegmn1l  35372  rngohomco  35405  rngoisocnv  35412  rngoisoco  35413  crngohomfo  35437  isidlc  35446  rngoidl  35455  prnc  35498  ispridlc  35501  cvrval2  36563  glbconxN  36667  hlrelat5N  36690  cvratlem  36710  cvrat2  36718  athgt  36745  3dim2  36757  llnn0  36805  lplnn0N  36836  lvoln0N  36880  snatpsubN  37039  paddasslem18  37126  pmod1i  37137  lhpexle2  37299  lhpexle3lem  37300  lhpexle3  37301  ldilcnv  37404  trlcnv  37454  trlnidatb  37466  cdleme32snaw  37724  cdleme32fvaw  37728  cdleme42ke  37774  cdlemeg46gf  37822  cdleme50trn12  37841  cdlemg1cex  37877  cdlemb3  37895  tgrpgrplem  38038  tgrpabl  38040  tendoplcl2  38067  tendo0pl  38080  tendoicl  38085  tendoipl  38086  cdlemkid3N  38222  tendoex  38264  erngdvlem4  38280  erngdvlem4-rN  38288  dib1dim  38454  dib1dim2  38457  dihglbcpreN  38589  dihmeetALTN  38616  dih1dimatlem  38618  dihatlat  38623  fzindd  39256  lcmineqlem1  39310  lcmineqlem3  39312  metakunt29  39369  metakunt30  39370  factwoffsmonot  39375  oddcomabszz  39872  acongtr  39906  rpnnen3lem  39959  islssfg  40001  lmhmfgsplit  40017  unxpwdom3  40026  hbtlem7  40056  iocmbl  40150  ss2iundf  40347  ismnu  40956  grumnudlem  40980  nzss  41008  dvconstbi  41025  bccbc  41036  uzmptshftfval  41037  iccdifprioo  42140  climisp  42375  limsupresxr  42395  liminfresxr  42396  dvnmul  42572  volico  42612  volioore  42619  fourierdlem74  42809  fourierdlem75  42810  sge0iunmptlemfi  43039  sge0iunmptlemre  43041  sge0iunmpt  43044  sge0xp  43055  hspmbllem2  43253  smflimlem3  43393  smfsupmpt  43433  smfinflem  43435  smfinfmpt  43437  smflimsupmpt  43447  smfliminfmpt  43450  funressnbrafv2  43787  uniimaelsetpreimafv  43900  imasetpreimafvbijlemfv1  43907  imasetpreimafvbijlemfo  43909  sprsymrelfo  44001  nnsum4primesodd  44301  nnsum4primesoddALTV  44302  nn0mnd  44426  rnghmsubcsetclem2  44587  rhmsubcsetclem2  44633  rhmsubcrngclem2  44639  lcoss  44832  snlindsntorlem  44866  aacllem  45316
  Copyright terms: Public domain W3C validator