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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 477 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1080 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  simpl1r  1111  simpr1r  1117  simp11r  1171  simp21r  1177  simp31r  1183  vtoclgftOLD  3250  funprgOLD  5929  omeulem2  7648  uniinqs  7812  unxpdomlem3  8151  elfiun  8321  cofsmo  9076  isfin2-2  9126  isf32lem9  9168  tskun  9593  tskurn  9596  reclem3pr  9856  dedekind  10185  dmdcan  10720  lt2msq1  10892  supmullem1  10978  supmul  10980  xaddass2  12065  xlt2add  12075  xmulasslem3  12101  iccsplit  12290  expaddzlem  12886  expaddz  12887  expmulz  12889  limsupgle  14189  o1add  14325  o1mul  14326  o1sub  14327  bitsfzo  15138  sadfval  15155  smufval  15180  prmexpb  15411  4sqlem18  15647  vdwlem10  15675  setsstruct2  15877  mrieqv2d  16280  curf1  16846  mndodcong  17942  subgabl  18222  gex2abl  18235  cntzsubr  18793  abvres  18820  lbsind2  19062  lbsextlem2  19140  lbsextg  19143  matring  20230  mdetunilem8  20406  maducoeval  20426  maducoeval2  20427  madurid  20431  cramerimplem3  20472  pmatcollpw2  20564  pm2mpf1  20585  cnprest  21074  isreg2  21162  fbssfi  21622  hausflimlem  21764  tmdgsum  21880  ssblps  22208  ssbl  22209  xrsmopn  22596  cphassi  22995  cphassir  22996  4cphipval2  23022  cphipval  23023  dvres2  23657  vieta1  24048  aalioulem4  24071  efgh  24268  cxpadd  24406  cxpsub  24409  divcxp  24414  cxple2  24424  cxplt2  24425  cxpcn3lem  24469  angcan  24513  ang180lem5  24524  isosctrlem3  24531  lgssq  25043  brbtwn2  25766  axcontlem4  25828  axcontlem8  25832  uhgr2edg  26081  chscllem4  28469  ogrpinvlt  29698  pstmval  29912  measinblem  30257  cvmlift2lem6  31264  eqfunresadj  31635  poseq  31724  noetalem5  31841  linethru  32235  cnres2  33533  lcv1  34147  lfl1  34176  lshpkrex  34224  hlrelat3  34517  cvrval3  34518  cvrval4N  34519  athgt  34561  atcvrlln2  34624  atcvrlln  34625  lvolnle3at  34687  lvolnlelpln  34690  4atlem11  34714  4atlem12  34717  2lplnj  34725  dalemddea  34789  cdlema2N  34897  paddasslem2  34926  atmod1i1m  34963  lhp2lt  35106  lhp0lt  35108  lhpexle3lem  35116  lhpj1  35127  lhpmcvr4N  35131  lhpelim  35142  lhpmod2i2  35143  lhpmod6i1  35144  cdlemb2  35146  lhpat  35148  ltrnatb  35242  ltrnel  35244  ltrncnvel  35247  ltrncnv  35251  ltrnmwOLD  35257  trlval2  35269  trljat1  35272  trljat2  35273  trlnidatb  35283  cdlemc1  35297  cdlemc2  35298  cdlemc5  35301  cdlemc6  35302  cdleme0aa  35316  cdleme0b  35318  cdleme0c  35319  cdleme0e  35323  cdleme0fN  35324  cdleme01N  35327  cdleme0ex1N  35329  cdleme0moN  35331  cdleme3g  35340  cdleme3h  35341  cdleme3  35343  cdleme4  35344  cdleme4a  35345  cdleme5  35346  cdleme8  35356  cdleme9  35359  cdleme10  35360  cdleme16aN  35365  cdleme11fN  35370  cdleme11g  35371  cdleme11k  35374  cdleme13  35378  cdleme17c  35394  cdleme17d1  35395  cdleme18c  35399  cdleme22gb  35400  cdlemeda  35404  cdlemednpq  35405  cdlemednuN  35406  cdleme19c  35412  cdleme20aN  35416  cdleme20bN  35417  cdleme20c  35418  cdleme22aa  35446  cdleme22d  35450  cdleme22e  35451  cdleme27cl  35473  cdleme27a  35474  cdleme30a  35485  cdleme42a  35578  cdleme42c  35579  cdlemg2fv2  35707  cdlemg2m  35711  cdlemg4g  35723  cdlemg4  35724  cdlemg6c  35727  cdlemg7aN  35732  cdlemg9a  35739  cdlemg9b  35740  cdlemg10c  35746  cdlemg12a  35750  cdlemg12b  35751  cdlemg17a  35768  cdlemg18b  35786  cdlemg18c  35787  trlcoabs2N  35829  trlcolem  35833  tendoco2  35875  tendoicl  35903  cdlemi1  35925  cdlemi2  35926  cdlemj3  35930  tendocan  35931  cdlemk3  35940  cdlemk4  35941  cdlemk5a  35942  cdlemk9  35946  cdlemk9bN  35947  cdlemk10  35950  cdlemk30  36001  cdlemk31  36003  cdlemk39  36023  cdlemkfid1N  36028  cdlemkfid2N  36030  cdlemk19ylem  36037  cdlemk19xlem  36049  cdlemk53b  36063  cdlemk53  36064  cdlemk55a  36066  cdlemk43N  36070  cdlemk19u1  36076  cdlemm10N  36226  cdlemn2  36303  cdlemn10  36314  dihjustlem  36324  dihord2cN  36329  dihvalcq2  36355  dihopelvalcpre  36356  dihord5b  36367  dihord6b  36368  dihmeetlem2N  36407  dihmeetbclemN  36412  dihmeetlem4preN  36414  dihmeetALTN  36435  dochshpncl  36492  dochsatshpb  36560  hdmapval3N  36949  hgmap11  37013  pellfundex  37269  congtr  37351  fzmaxdif  37367  isnumbasgrplem2  37493  idomsubgmo  37595  ntrclsk13  38189  restuni3  39121  unirnmapsn  39222  ssmapsn  39224  infnsuprnmpt  39281  upbdrech  39332  suplesup  39368  infleinf  39401  supxrunb3  39436  mullimc  39648  islptre  39651  mullimcf  39655  neglimc  39679  limsupmnfuzlem  39758  limsupre3lem  39764  limsupre3uzlem  39767  icccncfext  39863  dvmptfprod  39923  stoweidlem31  40011  opnvonmbllem2  40610  smflimsuplem7  40795  prmdvdsfmtnof1lem1  41261  domnmsuppn0  41915  mndpfsupp  41922  lincext3  42010
  Copyright terms: Public domain W3C validator