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

Theorem simp1r 1195
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1r (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 488 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1130 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-an 400  df-3an 1086
This theorem is referenced by:  simp11r  1282  simp21r  1288  simp31r  1294  offsplitfpar  7811  omeulem2  8205  uniinqs  8373  unxpdomlem3  8721  elfiun  8891  cofsmo  9689  isfin2-2  9739  isf32lem9  9781  tskun  10206  tskurn  10209  reclem3pr  10469  dedekind  10801  subaddmulsub  11101  dmdcan  11348  lt2msq1  11522  supmullem1  11607  supmul  11609  xaddass2  12640  xlt2add  12650  xmulasslem3  12676  iccsplit  12872  expaddzlem  13477  expaddz  13478  expmulz  13480  limsupgle  14834  o1add  14970  o1mul  14971  o1sub  14972  bitsfzo  15782  sadfval  15799  smufval  15824  prmexpb  16060  4sqlem18  16296  vdwlem10  16324  setsstruct2  16521  mrieqv2d  16910  curf1  17475  mgmsscl  17857  mndodcong  18670  subgabl  18956  gex2abl  18971  cntzsubr  19568  abvres  19610  lbsind2  19853  lbsextlem2  19931  lbsextg  19934  matring  21055  mdetunilem8  21231  maducoeval  21251  maducoeval2  21252  madurid  21256  cramerimplem3  21297  pmatcollpw2  21389  pm2mpf1  21410  cnprest  21900  isreg2  21988  fbssfi  22448  hausflimlem  22590  tmdgsum  22706  ssblps  23035  ssbl  23036  xrsmopn  23423  cphassi  23825  cphassir  23826  4cphipval2  23852  cphipval  23853  dvres2  24521  vieta1  24914  aalioulem4  24937  efgh  25139  cxpadd  25276  cxpsub  25279  divcxp  25284  cxple2  25294  cxplt2  25295  cxpcn3lem  25342  angcan  25394  ang180lem5  25405  isosctrlem3  25412  lgssq  25927  brbtwn2  26705  axcontlem4  26767  axcontlem8  26771  uhgr2edg  27004  chscllem4  29429  cshwrnid  30649  ogrpinvlt  30759  pstmval  31198  measinblem  31539  cvmlift2lem6  32615  eqfunresadj  33064  poseq  33155  noetalem5  33281  linethru  33674  cnres2  35149  lcv1  36285  lfl1  36314  lshpkrex  36362  hlrelat3  36656  cvrval3  36657  cvrval4N  36658  athgt  36700  atcvrlln2  36763  atcvrlln  36764  lvolnle3at  36826  lvolnlelpln  36829  4atlem11  36853  4atlem12  36856  2lplnj  36864  dalemddea  36928  cdlema2N  37036  paddasslem2  37065  atmod1i1m  37102  lhp2lt  37245  lhp0lt  37247  lhpexle3lem  37255  lhpj1  37266  lhpmcvr4N  37270  lhpelim  37281  lhpmod2i2  37282  lhpmod6i1  37283  cdlemb2  37285  lhpat  37287  ltrnatb  37381  ltrnel  37383  ltrncnvel  37386  ltrncnv  37390  trlval2  37407  trljat1  37410  trljat2  37411  trlnidatb  37421  cdlemc1  37435  cdlemc2  37436  cdlemc5  37439  cdlemc6  37440  cdleme0aa  37454  cdleme0b  37456  cdleme0c  37457  cdleme0e  37461  cdleme0fN  37462  cdleme01N  37465  cdleme0ex1N  37467  cdleme0moN  37469  cdleme3g  37478  cdleme3h  37479  cdleme3  37481  cdleme4  37482  cdleme4a  37483  cdleme5  37484  cdleme8  37494  cdleme9  37497  cdleme10  37498  cdleme16aN  37503  cdleme11fN  37508  cdleme11g  37509  cdleme11k  37512  cdleme13  37516  cdleme17c  37532  cdleme17d1  37533  cdleme18c  37537  cdleme22gb  37538  cdlemeda  37542  cdlemednpq  37543  cdlemednuN  37544  cdleme19c  37549  cdleme20aN  37553  cdleme20bN  37554  cdleme20c  37555  cdleme22aa  37583  cdleme22d  37587  cdleme22e  37588  cdleme27cl  37610  cdleme27a  37611  cdleme30a  37622  cdleme42a  37715  cdleme42c  37716  cdlemg2fv2  37844  cdlemg2m  37848  cdlemg4g  37860  cdlemg4  37861  cdlemg6c  37864  cdlemg7aN  37869  cdlemg9a  37876  cdlemg9b  37877  cdlemg10c  37883  cdlemg12a  37887  cdlemg12b  37888  cdlemg17a  37905  cdlemg18b  37923  cdlemg18c  37924  trlcoabs2N  37966  trlcolem  37970  tendoco2  38012  tendoicl  38040  cdlemi1  38062  cdlemi2  38063  cdlemj3  38067  tendocan  38068  cdlemk3  38077  cdlemk4  38078  cdlemk5a  38079  cdlemk9  38083  cdlemk9bN  38084  cdlemk10  38087  cdlemk30  38138  cdlemk31  38140  cdlemk39  38160  cdlemkfid1N  38165  cdlemkfid2N  38167  cdlemk19ylem  38174  cdlemk19xlem  38186  cdlemk53b  38200  cdlemk53  38201  cdlemk55a  38203  cdlemk43N  38207  cdlemk19u1  38213  cdlemm10N  38362  cdlemn2  38439  cdlemn10  38450  dihjustlem  38460  dihord2cN  38465  dihvalcq2  38491  dihopelvalcpre  38492  dihord5b  38503  dihord6b  38504  dihmeetlem2N  38543  dihmeetbclemN  38548  dihmeetlem4preN  38550  dihmeetALTN  38571  dochshpncl  38628  dochsatshpb  38696  hdmapval3N  39082  hgmap11  39146  nn0rppwr  39424  remulcand  39507  pellfundex  39747  congtr  39826  fzmaxdif  39842  isnumbasgrplem2  39968  idomsubgmo  40062  ntrclsk13  40697  grumnudlem  40917  restuni3  41679  unirnmapsn  41772  ssmapsn  41774  infnsuprnmpt  41817  upbdrech  41867  suplesup  41901  infleinf  41934  supxrunb3  41966  mullimc  42188  islptre  42191  mullimcf  42195  neglimc  42219  limsupmnfuzlem  42298  limsupre3lem  42304  limsupre3uzlem  42307  icccncfext  42459  dvmptfprod  42517  stoweidlem31  42603  opnvonmbllem2  43202  smflimsuplem7  43387  funressneu  43569  prmdvdsfmtnof1lem1  44031  domnmsuppn0  44701  mndpfsupp  44708  lincext3  44795  2arymaptfo  44998
  Copyright terms: Public domain W3C validator