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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 485 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1125 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp11r  1277  simp21r  1283  simp31r  1289  offsplitfpar  7806  omeulem2  8199  uniinqs  8367  unxpdomlem3  8713  elfiun  8883  cofsmo  9680  isfin2-2  9730  isf32lem9  9772  tskun  10197  tskurn  10200  reclem3pr  10460  dedekind  10792  subaddmulsub  11092  dmdcan  11339  lt2msq1  11513  supmullem1  11600  supmul  11602  xaddass2  12633  xlt2add  12643  xmulasslem3  12669  iccsplit  12861  expaddzlem  13462  expaddz  13463  expmulz  13465  limsupgle  14824  o1add  14960  o1mul  14961  o1sub  14962  bitsfzo  15774  sadfval  15791  smufval  15816  prmexpb  16052  4sqlem18  16288  vdwlem10  16316  setsstruct2  16511  mrieqv2d  16900  curf1  17465  mgmsscl  17847  mndodcong  18601  subgabl  18887  gex2abl  18902  cntzsubr  19499  abvres  19541  lbsind2  19784  lbsextlem2  19862  lbsextg  19865  matring  20982  mdetunilem8  21158  maducoeval  21178  maducoeval2  21179  madurid  21183  cramerimplem3  21224  pmatcollpw2  21316  pm2mpf1  21337  cnprest  21827  isreg2  21915  fbssfi  22375  hausflimlem  22517  tmdgsum  22633  ssblps  22961  ssbl  22962  xrsmopn  23349  cphassi  23747  cphassir  23748  4cphipval2  23774  cphipval  23775  dvres2  24439  vieta1  24830  aalioulem4  24853  efgh  25052  cxpadd  25189  cxpsub  25192  divcxp  25197  cxple2  25207  cxplt2  25208  cxpcn3lem  25255  angcan  25307  ang180lem5  25318  isosctrlem3  25325  lgssq  25841  brbtwn2  26619  axcontlem4  26681  axcontlem8  26685  uhgr2edg  26918  chscllem4  29345  cshwrnid  30563  ogrpinvlt  30652  pstmval  31035  measinblem  31379  cvmlift2lem6  32453  eqfunresadj  32902  poseq  32993  noetalem5  33119  linethru  33512  cnres2  34924  lcv1  36059  lfl1  36088  lshpkrex  36136  hlrelat3  36430  cvrval3  36431  cvrval4N  36432  athgt  36474  atcvrlln2  36537  atcvrlln  36538  lvolnle3at  36600  lvolnlelpln  36603  4atlem11  36627  4atlem12  36630  2lplnj  36638  dalemddea  36702  cdlema2N  36810  paddasslem2  36839  atmod1i1m  36876  lhp2lt  37019  lhp0lt  37021  lhpexle3lem  37029  lhpj1  37040  lhpmcvr4N  37044  lhpelim  37055  lhpmod2i2  37056  lhpmod6i1  37057  cdlemb2  37059  lhpat  37061  ltrnatb  37155  ltrnel  37157  ltrncnvel  37160  ltrncnv  37164  trlval2  37181  trljat1  37184  trljat2  37185  trlnidatb  37195  cdlemc1  37209  cdlemc2  37210  cdlemc5  37213  cdlemc6  37214  cdleme0aa  37228  cdleme0b  37230  cdleme0c  37231  cdleme0e  37235  cdleme0fN  37236  cdleme01N  37239  cdleme0ex1N  37241  cdleme0moN  37243  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme4  37256  cdleme4a  37257  cdleme5  37258  cdleme8  37268  cdleme9  37271  cdleme10  37272  cdleme16aN  37277  cdleme11fN  37282  cdleme11g  37283  cdleme11k  37286  cdleme13  37290  cdleme17c  37306  cdleme17d1  37307  cdleme18c  37311  cdleme22gb  37312  cdlemeda  37316  cdlemednpq  37317  cdlemednuN  37318  cdleme19c  37323  cdleme20aN  37327  cdleme20bN  37328  cdleme20c  37329  cdleme22aa  37357  cdleme22d  37361  cdleme22e  37362  cdleme27cl  37384  cdleme27a  37385  cdleme30a  37396  cdleme42a  37489  cdleme42c  37490  cdlemg2fv2  37618  cdlemg2m  37622  cdlemg4g  37634  cdlemg4  37635  cdlemg6c  37638  cdlemg7aN  37643  cdlemg9a  37650  cdlemg9b  37651  cdlemg10c  37657  cdlemg12a  37661  cdlemg12b  37662  cdlemg17a  37679  cdlemg18b  37697  cdlemg18c  37698  trlcoabs2N  37740  trlcolem  37744  tendoco2  37786  tendoicl  37814  cdlemi1  37836  cdlemi2  37837  cdlemj3  37841  tendocan  37842  cdlemk3  37851  cdlemk4  37852  cdlemk5a  37853  cdlemk9  37857  cdlemk9bN  37858  cdlemk10  37861  cdlemk30  37912  cdlemk31  37914  cdlemk39  37934  cdlemkfid1N  37939  cdlemkfid2N  37941  cdlemk19ylem  37948  cdlemk19xlem  37960  cdlemk53b  37974  cdlemk53  37975  cdlemk55a  37977  cdlemk43N  37981  cdlemk19u1  37987  cdlemm10N  38136  cdlemn2  38213  cdlemn10  38224  dihjustlem  38234  dihord2cN  38239  dihvalcq2  38265  dihopelvalcpre  38266  dihord5b  38277  dihord6b  38278  dihmeetlem2N  38317  dihmeetbclemN  38322  dihmeetlem4preN  38324  dihmeetALTN  38345  dochshpncl  38402  dochsatshpb  38470  hdmapval3N  38856  hgmap11  38920  nn0rppwr  39062  remulcand  39130  pellfundex  39363  congtr  39442  fzmaxdif  39458  isnumbasgrplem2  39584  idomsubgmo  39678  ntrclsk13  40301  grumnudlem  40501  restuni3  41265  unirnmapsn  41357  ssmapsn  41359  infnsuprnmpt  41402  upbdrech  41452  suplesup  41487  infleinf  41520  supxrunb3  41552  mullimc  41777  islptre  41780  mullimcf  41784  neglimc  41808  limsupmnfuzlem  41887  limsupre3lem  41893  limsupre3uzlem  41896  icccncfext  42050  dvmptfprod  42110  stoweidlem31  42197  opnvonmbllem2  42796  smflimsuplem7  42981  funressneu  43163  prmdvdsfmtnof1lem1  43593  domnmsuppn0  44315  mndpfsupp  44322  lincext3  44409
  Copyright terms: Public domain W3C validator