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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 486 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1134 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  simp11r  1286  simp21r  1292  simp31r  1298  eqfunresadj  7310  offsplitfpar  8056  poseq  8095  omeulem2  8535  uniinqs  8743  unxpdomlem3  9203  elfiun  9373  cofsmo  10212  isfin2-2  10262  isf32lem9  10304  tskun  10729  tskurn  10732  reclem3pr  10992  dedekind  11325  subaddmulsub  11625  dmdcan  11872  lt2msq1  12046  supmullem1  12132  supmul  12134  xaddass2  13176  xlt2add  13186  xmulasslem3  13212  iccsplit  13409  expaddzlem  14018  expaddz  14019  expmulz  14021  limsupgle  15366  o1add  15503  o1mul  15504  o1sub  15505  bitsfzo  16322  sadfval  16339  smufval  16364  prmexpb  16603  4sqlem18  16841  vdwlem10  16869  setsstruct2  17053  mrieqv2d  17526  curf1  18121  mgmsscl  18509  mndodcong  19331  subgabl  19621  gex2abl  19636  cntzsubr  20271  abvres  20314  lbsind2  20558  lbsextlem2  20636  lbsextg  20639  matring  21808  mdetunilem8  21984  maducoeval  22004  maducoeval2  22005  madurid  22009  cramerimplem3  22050  pmatcollpw2  22143  pm2mpf1  22164  cnprest  22656  isreg2  22744  fbssfi  23204  hausflimlem  23346  tmdgsum  23462  ssblps  23791  ssbl  23792  xrsmopn  24191  cphassi  24594  cphassir  24595  4cphipval2  24622  cphipval  24623  dvres2  25292  vieta1  25688  aalioulem4  25711  efgh  25913  cxpadd  26050  cxpsub  26053  divcxp  26058  cxple2  26068  cxplt2  26069  cxpcn3lem  26116  angcan  26168  ang180lem5  26179  isosctrlem3  26186  lgssq  26701  nosupinfsep  27096  noetalem1  27105  noeta2  27146  sltlpss  27258  brbtwn2  27896  axcontlem4  27958  axcontlem8  27962  uhgr2edg  28198  chscllem4  30624  cshwrnid  31857  ogrpinvlt  31973  pstmval  32516  measinblem  32859  cvmlift2lem6  33942  linethru  34767  cnres2  36251  lcv1  37532  lfl1  37561  lshpkrex  37609  hlrelat3  37904  cvrval3  37905  cvrval4N  37906  athgt  37948  atcvrlln2  38011  atcvrlln  38012  lvolnle3at  38074  lvolnlelpln  38077  4atlem11  38101  4atlem12  38104  2lplnj  38112  dalemddea  38176  cdlema2N  38284  paddasslem2  38313  atmod1i1m  38350  lhp2lt  38493  lhp0lt  38495  lhpexle3lem  38503  lhpj1  38514  lhpmcvr4N  38518  lhpelim  38529  lhpmod2i2  38530  lhpmod6i1  38531  cdlemb2  38533  lhpat  38535  ltrnatb  38629  ltrnel  38631  ltrncnvel  38634  ltrncnv  38638  trlval2  38655  trljat1  38658  trljat2  38659  trlnidatb  38669  cdlemc1  38683  cdlemc2  38684  cdlemc5  38687  cdlemc6  38688  cdleme0aa  38702  cdleme0b  38704  cdleme0c  38705  cdleme0e  38709  cdleme0fN  38710  cdleme01N  38713  cdleme0ex1N  38715  cdleme0moN  38717  cdleme3g  38726  cdleme3h  38727  cdleme3  38729  cdleme4  38730  cdleme4a  38731  cdleme5  38732  cdleme8  38742  cdleme9  38745  cdleme10  38746  cdleme16aN  38751  cdleme11fN  38756  cdleme11g  38757  cdleme11k  38760  cdleme13  38764  cdleme17c  38780  cdleme17d1  38781  cdleme18c  38785  cdleme22gb  38786  cdlemeda  38790  cdlemednpq  38791  cdlemednuN  38792  cdleme19c  38797  cdleme20aN  38801  cdleme20bN  38802  cdleme20c  38803  cdleme22aa  38831  cdleme22d  38835  cdleme22e  38836  cdleme27cl  38858  cdleme27a  38859  cdleme30a  38870  cdleme42a  38963  cdleme42c  38964  cdlemg2fv2  39092  cdlemg2m  39096  cdlemg4g  39108  cdlemg4  39109  cdlemg6c  39112  cdlemg7aN  39117  cdlemg9a  39124  cdlemg9b  39125  cdlemg10c  39131  cdlemg12a  39135  cdlemg12b  39136  cdlemg17a  39153  cdlemg18b  39171  cdlemg18c  39172  trlcoabs2N  39214  trlcolem  39218  tendoco2  39260  tendoicl  39288  cdlemi1  39310  cdlemi2  39311  cdlemj3  39315  tendocan  39316  cdlemk3  39325  cdlemk4  39326  cdlemk5a  39327  cdlemk9  39331  cdlemk9bN  39332  cdlemk10  39335  cdlemk30  39386  cdlemk31  39388  cdlemk39  39408  cdlemkfid1N  39413  cdlemkfid2N  39415  cdlemk19ylem  39422  cdlemk19xlem  39434  cdlemk53b  39448  cdlemk53  39449  cdlemk55a  39451  cdlemk43N  39455  cdlemk19u1  39461  cdlemm10N  39610  cdlemn2  39687  cdlemn10  39698  dihjustlem  39708  dihord2cN  39713  dihvalcq2  39739  dihopelvalcpre  39740  dihord5b  39751  dihord6b  39752  dihmeetlem2N  39791  dihmeetbclemN  39796  dihmeetlem4preN  39798  dihmeetALTN  39819  dochshpncl  39876  dochsatshpb  39944  hdmapval3N  40330  hgmap11  40394  nn0rppwr  40848  remulcand  40936  pellfundex  41238  congtr  41318  fzmaxdif  41334  isnumbasgrplem2  41460  idomsubgmo  41554  ntrclsk13  42417  grumnudlem  42639  restuni3  43402  unirnmapsn  43509  ssmapsn  43511  infnsuprnmpt  43552  upbdrech  43613  suplesup  43647  infleinf  43680  supxrunb3  43708  mullimc  43931  islptre  43934  mullimcf  43938  neglimc  43962  limsupmnfuzlem  44041  limsupre3lem  44047  limsupre3uzlem  44050  icccncfext  44202  dvmptfprod  44260  stoweidlem31  44346  opnvonmbllem2  44948  smflimsuplem7  45141  funressneu  45355  cfsetsnfsetf1  45367  prmdvdsfmtnof1lem1  45850  domnmsuppn0  46519  mndpfsupp  46526  lincext3  46611  2arymaptfo  46814
  Copyright terms: Public domain W3C validator