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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 473 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1156 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-an 385  df-3an 1102
This theorem is referenced by:  simpl1rOLD  1289  simpr1rOLD  1301  simp11r  1377  simp21r  1383  simp31r  1389  omeulem2  7910  uniinqs  8072  unxpdomlem3  8415  elfiun  8585  cofsmo  9386  isfin2-2  9436  isf32lem9  9478  tskun  9903  tskurn  9906  reclem3pr  10166  dedekind  10495  dmdcan  11030  lt2msq1  11202  supmullem1  11288  supmul  11290  xaddass2  12318  xlt2add  12328  xmulasslem3  12354  iccsplit  12548  expaddzlem  13146  expaddz  13147  expmulz  13149  limsupgle  14451  o1add  14587  o1mul  14588  o1sub  14589  bitsfzo  15396  sadfval  15413  smufval  15438  prmexpb  15667  4sqlem18  15903  vdwlem10  15931  setsstruct2  16127  mrieqv2d  16524  curf1  17090  mndodcong  18182  subgabl  18462  gex2abl  18475  cntzsubr  19036  abvres  19063  lbsind2  19308  lbsextlem2  19388  lbsextg  19391  matring  20480  mdetunilem8  20657  maducoeval  20677  maducoeval2  20678  madurid  20682  cramerimplem3  20725  pmatcollpw2  20817  pm2mpf1  20838  cnprest  21328  isreg2  21416  fbssfi  21875  hausflimlem  22017  tmdgsum  22133  ssblps  22461  ssbl  22462  xrsmopn  22849  cphassi  23247  cphassir  23248  4cphipval2  23274  cphipval  23275  dvres2  23913  vieta1  24304  aalioulem4  24327  efgh  24525  cxpadd  24662  cxpsub  24665  divcxp  24670  cxple2  24680  cxplt2  24681  cxpcn3lem  24725  angcan  24769  ang180lem5  24780  isosctrlem3  24787  lgssq  25299  brbtwn2  26022  axcontlem4  26084  axcontlem8  26088  uhgr2edg  26338  chscllem4  28850  ogrpinvlt  30072  pstmval  30286  measinblem  30631  cvmlift2lem6  31635  eqfunresadj  32003  poseq  32096  noetalem5  32210  linethru  32603  cnres2  33892  lcv1  34840  lfl1  34869  lshpkrex  34917  hlrelat3  35211  cvrval3  35212  cvrval4N  35213  athgt  35255  atcvrlln2  35318  atcvrlln  35319  lvolnle3at  35381  lvolnlelpln  35384  4atlem11  35408  4atlem12  35411  2lplnj  35419  dalemddea  35483  cdlema2N  35591  paddasslem2  35620  atmod1i1m  35657  lhp2lt  35800  lhp0lt  35802  lhpexle3lem  35810  lhpj1  35821  lhpmcvr4N  35825  lhpelim  35836  lhpmod2i2  35837  lhpmod6i1  35838  cdlemb2  35840  lhpat  35842  ltrnatb  35936  ltrnel  35938  ltrncnvel  35941  ltrncnv  35945  trlval2  35962  trljat1  35965  trljat2  35966  trlnidatb  35976  cdlemc1  35990  cdlemc2  35991  cdlemc5  35994  cdlemc6  35995  cdleme0aa  36009  cdleme0b  36011  cdleme0c  36012  cdleme0e  36016  cdleme0fN  36017  cdleme01N  36020  cdleme0ex1N  36022  cdleme0moN  36024  cdleme3g  36033  cdleme3h  36034  cdleme3  36036  cdleme4  36037  cdleme4a  36038  cdleme5  36039  cdleme8  36049  cdleme9  36052  cdleme10  36053  cdleme16aN  36058  cdleme11fN  36063  cdleme11g  36064  cdleme11k  36067  cdleme13  36071  cdleme17c  36087  cdleme17d1  36088  cdleme18c  36092  cdleme22gb  36093  cdlemeda  36097  cdlemednpq  36098  cdlemednuN  36099  cdleme19c  36104  cdleme20aN  36108  cdleme20bN  36109  cdleme20c  36110  cdleme22aa  36138  cdleme22d  36142  cdleme22e  36143  cdleme27cl  36165  cdleme27a  36166  cdleme30a  36177  cdleme42a  36270  cdleme42c  36271  cdlemg2fv2  36399  cdlemg2m  36403  cdlemg4g  36415  cdlemg4  36416  cdlemg6c  36419  cdlemg7aN  36424  cdlemg9a  36431  cdlemg9b  36432  cdlemg10c  36438  cdlemg12a  36442  cdlemg12b  36443  cdlemg17a  36460  cdlemg18b  36478  cdlemg18c  36479  trlcoabs2N  36521  trlcolem  36525  tendoco2  36567  tendoicl  36595  cdlemi1  36617  cdlemi2  36618  cdlemj3  36622  tendocan  36623  cdlemk3  36632  cdlemk4  36633  cdlemk5a  36634  cdlemk9  36638  cdlemk9bN  36639  cdlemk10  36642  cdlemk30  36693  cdlemk31  36695  cdlemk39  36715  cdlemkfid1N  36720  cdlemkfid2N  36722  cdlemk19ylem  36729  cdlemk19xlem  36741  cdlemk53b  36755  cdlemk53  36756  cdlemk55a  36758  cdlemk43N  36762  cdlemk19u1  36768  cdlemm10N  36917  cdlemn2  36994  cdlemn10  37005  dihjustlem  37015  dihord2cN  37020  dihvalcq2  37046  dihopelvalcpre  37047  dihord5b  37058  dihord6b  37059  dihmeetlem2N  37098  dihmeetbclemN  37103  dihmeetlem4preN  37105  dihmeetALTN  37126  dochshpncl  37183  dochsatshpb  37251  hdmapval3N  37637  hgmap11  37701  pellfundex  37970  congtr  38051  fzmaxdif  38067  isnumbasgrplem2  38193  idomsubgmo  38295  ntrclsk13  38887  restuni3  39811  unirnmapsn  39911  ssmapsn  39913  infnsuprnmpt  39966  upbdrech  40018  suplesup  40053  infleinf  40086  supxrunb3  40120  mullimc  40346  islptre  40349  mullimcf  40353  neglimc  40377  limsupmnfuzlem  40456  limsupre3lem  40462  limsupre3uzlem  40465  icccncfext  40598  dvmptfprod  40658  stoweidlem31  40745  opnvonmbllem2  41347  smflimsuplem7  41532  funressneu  41684  prmdvdsfmtnof1lem1  42089  domnmsuppn0  42736  mndpfsupp  42743  lincext3  42831
  Copyright terms: Public domain W3C validator