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

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

Proof of Theorem 3expa
StepHypRef Expression
1 df-3an 1102 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbir 226 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-3an 1102
This theorem is referenced by:  3exp  1141  ad4ant123  1206  ad4ant124  1208  ad4ant134  1210  ad4ant234  1212  ad5ant123  1469  3anidm23  1537  mp3an2  1566  mpd3an3  1579  rgen3  3164  moi2  3585  sbc3ie  3703  2if2  4332  preq12bg  4573  prel12gOLD  4574  ralxfrd2  5081  reuhypd  5092  otsndisj  5174  funcnvqp  6164  fvtp1g  6688  fntpb  6698  f1imass  6745  weisoeq  6829  f1ofveu  6869  f1ocnvfv3  6870  curry1f  7505  curry2f  7507  funsssuppss  7556  tfrlem11  7720  oalimcl  7877  oeordsuc  7911  oelim2  7912  nneob  7969  mapxpen  8365  findcard  8438  wemaplem3  8692  en2eqpr  9113  infxpabs  9319  infxp  9322  cfflb  9366  cfsmolem  9377  isf32lem12  9471  fin1a2lem9  9515  fin1a2s  9521  axcc3  9545  axdc3lem4  9560  zornn0g  9612  pwfseqlem4  9769  tskwun  9891  tskint  9892  tskxp  9894  tskmap  9895  gruf  9918  gruwun  9920  grutsk1  9928  addcanpi  10006  ltapi  10010  mul4  10490  add4  10541  2addsub  10580  addsubeq4  10581  muladd  10747  ltleadd  10796  receu  10957  p1le  11151  lemul12b  11165  lbinf  11261  zdiv  11713  fzind  11741  fnn0ind  11742  uzss  11925  zbtwnre  12005  qmulcl  12025  qreccl  12027  xrlttr  12189  xaddass  12297  xmulasslem3  12334  xmulass  12335  xadddilem  12342  xrsupsslem  12355  xrinfmsslem  12356  supxrunb1  12367  ixxin  12410  ioo0  12418  ico0  12439  ioc0  12440  icc0  12441  iooshf  12470  prunioo  12524  ioojoin  12526  elfz5  12557  elfz0fzfz0  12668  elfzonelfzo  12794  fzind2  12810  mulexpz  13123  expsub  13131  digit2  13220  digit1  13221  facndiv  13295  faclbnd4lem4  13303  faclbnd4  13304  faclbnd5  13305  bccmpl  13316  bcval5  13325  bcpasc  13328  hashunx  13393  hashdmpropge2  13482  ccatrn  13586  swrdccat1  13681  swrdccat2  13682  swrdswrd  13684  cats1un  13699  cshf1  13780  crim  14078  absmax  14292  ello12r  14471  elo12r  14482  climshftlem  14528  2sumeq2dv  14659  hash2iun  14777  expcnv  14818  2cprodeq2dv  14876  rpnnen2lem7  15169  dvdsval3  15207  dvdsnegb  15222  muldvds1  15229  muldvds2  15230  dvdscmul  15231  dvdsmulc  15232  dvdsmulcr  15234  dvds2ln  15237  divalgb  15347  ndvdssub  15352  gcddiv  15487  lcmfval  15553  lcmfcl  15560  dvdslcmf  15563  rpexp1i  15650  phiprmpw  15698  hashgcdeq  15711  pythagtriplem1  15738  pockthg  15827  infpnlem1  15831  4sqlem3  15871  0ramcl  15944  firest  16298  imasaddfnlem  16393  imasleval  16406  xpsfrn2  16435  mrerintcl  16462  iscatd  16538  fullestrcsetc  16996  fullsetcestrc  17011  clatleglb  17331  mreclatBAD  17392  pslem  17411  mrcmndind  17571  grplmulf1o  17694  grplactcnv  17723  mulgnn0subcl  17759  mulgsubcl  17760  mulgdir  17776  issubg2  17811  issubgrpd2  17812  cycsubgcl  17822  cycsubgss  17823  nmzsubg  17837  eqgen  17849  ghmmulg  17874  conjghm  17893  symgfixfo  18060  odeq  18170  odval2  18171  odf1  18180  dfod2  18182  gexdvds  18200  gexdvds2  18201  gexcl2  18205  gexdvds3  18206  sylow2blem2  18237  efgsp1  18351  efgrelexlemb  18364  mulgmhm  18434  mulgghm  18435  iscyggen2  18484  iscyg3  18489  srglmhm  18737  srgrmhm  18738  ringlghm  18806  ringrghm  18807  gsumdixp  18811  dvdsrcl2  18852  crngunit  18864  kerf1hrm  18947  subrgugrp  19003  cntzsubr  19016  lmodvsdir  19091  lmodvsass  19092  lmodvsghm  19128  lsssubg  19164  lss1d  19170  islbs2  19363  lidlsubg  19424  lidlsubcl  19425  quscrng  19449  lpigen  19465  xrsdsreval  19999  expghm  20052  mulgghm2  20053  ip0r  20192  obs2ss  20283  islindf3  20375  scmatscm  20530  scmataddcl  20533  scmatsubcl  20534  scmatfo  20547  matunit  20696  cpmatelimp  20730  cpmatelimp2  20732  cpmatinvcl  20735  cpmatmcl  20737  mat2pmatf  20746  m2cpmf  20760  cpm2mf  20770  m2cpmfo  20774  m2cpminv  20778  decpmataa0  20786  pm2mpf  20816  pm2mpf1  20817  idpm2idmp  20819  pm2mpfo  20832  elcls2  21092  opnnei  21138  innei  21143  iscnp4  21281  cnpnei  21282  iscncl  21287  cnnei  21300  cnconst  21302  ordthauslem  21401  bwth  21427  1stccnp  21479  llyrest  21502  nllyrest  21503  kgenss  21560  xkoccn  21636  kqsat  21748  kqt0lem  21753  isr0  21754  fbssfi  21854  isfild  21875  filconn  21900  trfilss  21906  fgtr  21907  ufileu  21936  ufilen  21947  fmfnfmlem4  21974  fmfnfm  21975  hausflimi  21997  cnpflf2  22017  cnpflf  22018  cnflf  22019  cnpfcf  22058  cnfcf  22059  cnextcn  22084  tmdmulg  22109  clsnsg  22126  tsmsxplem1  22169  tsmsxp  22171  ustuqtop0  22257  ismeti  22343  isxmet2d  22345  elbl2ps  22407  elbl2  22408  xblpnfps  22413  xblpnf  22414  xbln0  22432  blin  22439  blssexps  22444  blssex  22445  blsscls2  22522  blcls  22524  blsscls  22525  metss  22526  metrest  22542  metcn  22561  metustbl  22584  psmetutop  22585  nmf2  22610  ngpi  22645  tngngp3  22673  nmdvr  22687  nmoi  22745  nmoix  22746  nmoleub  22748  nghmcn  22762  xrsxmet  22825  iccntr  22837  metdsle  22868  icoopnst  22951  iocopnst  22952  icccvx  22962  pi1xfr  23067  isclmi0  23110  iscvsi  23141  cphipval  23254  lmmbr  23268  lmmbr2  23269  iscfil3  23283  iscau2  23287  cfilres  23306  bcthlem1  23333  bcthlem4  23336  bcthlem5  23337  rrxmet  23403  ioombl  23546  iccvolcl  23548  ioovolcl  23551  mbfi1fseqlem3  23698  mbfi1fseqlem4  23699  mbfi1fseqlem5  23700  ig1pcl  24149  ig1prsp  24151  aannenlem1  24297  taylplem1  24331  dvtaylp  24338  relogeftb  24545  logdivlt  24581  cxpexp  24628  rpcxpcl  24636  isppw2  25055  vmappw  25056  lgslem4  25239  lgscllem  25243  lgsneg1  25261  lgsne0  25274  cgraswap  25926  brbtwn2  25999  ax5seglem1  26022  ax5seglem2  26023  axcontlem4  26061  ewlkprop  26727  uspgr2wlkeq  26770  uhgrwkspthlem2  26878  clwlkclwwlkfo  27152  eupth2lem3lem7  27407  frgr3vlem2  27449  3cyclfrgrrn1  27460  4cycl2vnunb  27465  frgrncvvdeqlem8  27481  grpoidinvlem3  27689  isvciOLD  27763  nmcvcn  27878  ipval2lem2  27887  sspimsval  27921  isblo2  27966  nmoo0  27974  blocni  27988  isph  28005  sspph  28038  hvadd4  28221  hiassdi  28276  ocsh  28470  chj4  28722  spansncol  28755  pjjsi  28887  hoscl  28932  hodcl  28934  hoadd4  28971  homco1  28988  homulass  28989  hoadddi  28990  hoadddir  28991  unoplin  29107  adjvalval  29124  hmoplin  29129  bralnfn  29135  brafnmul  29138  lnopmi  29187  lnopcoi  29190  hmops  29207  hmopm  29208  nmophmi  29218  lnfncnbd  29244  cnlnadjlem2  29255  adjlnop  29273  adjmul  29279  adjadd  29280  branmfn  29292  kbass5  29307  kbass6  29308  leop2  29311  leopadd  29319  leopmuli  29320  pjimai  29363  atcvatlem  29572  chirredlem2  29578  mdsymlem3  29592  mdsymlem5  29594  sumdmdii  29602  sumdmdlem  29605  cdj3lem2a  29623  cdj3lem2b  29624  cdj3lem3a  29626  cdj3i  29628  xreceu  29955  toslublem  29992  tosglblem  29994  ogrpaddltbi  30044  archiabllem1b  30071  archiabllem2c  30074  archiabl  30077  slmdvsdir  30094  slmdvsass  30095  pstmxmet  30265  ordtconnlem1  30295  hasheuni  30472  omsf  30683  ballotlemirc  30918  signswmnd  30959  bnj1204  31403  txpconn  31537  cvmscld  31578  elmpps  31793  dfrdg2  32021  wsuclem  32091  nosepdm  32155  segconeu  32439  linecom  32578  linethru  32581  lineintmo  32585  fnemeet2  32683  fnejoin2  32685  lindsdom  33716  lindsenlbs  33717  matunitlindflem1  33718  matunitlindflem2  33719  heicant  33757  mblfinlem1  33759  mblfinlem3  33761  ismblfin  33763  cnambfre  33770  itg2addnclem2  33774  ftc1anclem1  33797  ftc1anclem5  33801  ftc1anclem6  33802  ftc2nc  33806  areacirclem2  33813  areacirclem4  33815  areacirclem5  33816  areacirc  33817  fzmul  33848  subspopn  33859  isbndx  33892  isbnd2  33893  isbnd3  33894  ssbnd  33898  prdstotbnd  33904  heibor1  33920  rrnmet  33939  rngonegmn1l  34051  rngohomco  34084  rngoisocnv  34091  rngoisoco  34092  crngohomfo  34116  isidlc  34125  rngoidl  34134  prnc  34177  ispridlc  34180  cvrval2  35054  glbconxN  35158  hlrelat5N  35181  cvratlem  35201  cvrat2  35209  athgt  35236  3dim2  35248  llnn0  35296  lplnn0N  35327  lvoln0N  35371  snatpsubN  35530  paddasslem18  35617  pmod1i  35628  lhpexle2  35790  lhpexle3lem  35791  lhpexle3  35792  ldilcnv  35895  trlcnv  35946  trlnidatb  35958  cdleme32snaw  36216  cdleme32fvaw  36220  cdleme42ke  36266  cdlemeg46gf  36314  cdleme50trn12  36333  cdlemg1cex  36369  cdlemb3  36387  tgrpgrplem  36530  tgrpabl  36532  tendoplcl2  36559  tendo0pl  36572  tendoicl  36577  tendoipl  36578  cdlemkid3N  36714  tendoex  36756  erngdvlem4  36772  erngdvlem4-rN  36780  dib1dim  36946  dib1dim2  36949  dihglbcpreN  37081  dihmeetALTN  37108  dih1dimatlem  37110  dihatlat  37115  oddcomabszz  38010  acongtr  38046  rpnnen3lem  38099  islssfg  38141  lmhmfgsplit  38157  unxpwdom3  38166  hbtlem7  38196  sdrgacs  38272  iocmbl  38298  ss2iundf  38451  nzss  39016  dvconstbi  39033  bccbc  39044  uzmptshftfval  39045  iccdifprioo  40223  climisp  40458  limsupresxr  40478  liminfresxr  40479  dvnmul  40638  volico  40679  volioore  40686  fourierdlem74  40876  fourierdlem75  40877  sge0iunmptlemfi  41109  sge0iunmptlemre  41111  sge0iunmpt  41114  sge0xp  41125  hspmbllem2  41323  smflimlem3  41463  smfsupmpt  41503  smfinflem  41505  smfinfmpt  41507  smflimsupmpt  41517  smfliminfmpt  41520  funressnbrafv2  41833  pfxccat1  41985  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  sprsymrelfo  42315  rnghmsubcsetclem2  42544  rhmsubcsetclem2  42590  rhmsubcrngclem2  42596  lcoss  42793  snlindsntorlem  42827  aacllem  43118
  Copyright terms: Public domain W3C validator