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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 476 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1102 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  simpl1r  1133  simpr1r  1139  simp11r  1193  simp21r  1199  simp31r  1205  vtoclgftOLD  3286  funprgOLD  5979  omeulem2  7708  uniinqs  7870  unxpdomlem3  8207  elfiun  8377  cofsmo  9129  isfin2-2  9179  isf32lem9  9221  tskun  9646  tskurn  9649  reclem3pr  9909  dedekind  10238  dmdcan  10773  lt2msq1  10945  supmullem1  11031  supmul  11033  xaddass2  12118  xlt2add  12128  xmulasslem3  12154  iccsplit  12343  expaddzlem  12943  expaddz  12944  expmulz  12946  limsupgle  14252  o1add  14388  o1mul  14389  o1sub  14390  bitsfzo  15204  sadfval  15221  smufval  15246  prmexpb  15477  4sqlem18  15713  vdwlem10  15741  setsstruct2  15943  mrieqv2d  16346  curf1  16912  mndodcong  18007  subgabl  18287  gex2abl  18300  cntzsubr  18860  abvres  18887  lbsind2  19129  lbsextlem2  19207  lbsextg  19210  matring  20297  mdetunilem8  20473  maducoeval  20493  maducoeval2  20494  madurid  20498  cramerimplem3  20539  pmatcollpw2  20631  pm2mpf1  20652  cnprest  21141  isreg2  21229  fbssfi  21688  hausflimlem  21830  tmdgsum  21946  ssblps  22274  ssbl  22275  xrsmopn  22662  cphassi  23060  cphassir  23061  4cphipval2  23087  cphipval  23088  dvres2  23721  vieta1  24112  aalioulem4  24135  efgh  24332  cxpadd  24470  cxpsub  24473  divcxp  24478  cxple2  24488  cxplt2  24489  cxpcn3lem  24533  angcan  24577  ang180lem5  24588  isosctrlem3  24595  lgssq  25107  brbtwn2  25830  axcontlem4  25892  axcontlem8  25896  uhgr2edg  26145  chscllem4  28627  ogrpinvlt  29852  pstmval  30066  measinblem  30411  cvmlift2lem6  31416  eqfunresadj  31785  poseq  31878  noetalem5  31992  linethru  32385  cnres2  33692  lcv1  34646  lfl1  34675  lshpkrex  34723  hlrelat3  35016  cvrval3  35017  cvrval4N  35018  athgt  35060  atcvrlln2  35123  atcvrlln  35124  lvolnle3at  35186  lvolnlelpln  35189  4atlem11  35213  4atlem12  35216  2lplnj  35224  dalemddea  35288  cdlema2N  35396  paddasslem2  35425  atmod1i1m  35462  lhp2lt  35605  lhp0lt  35607  lhpexle3lem  35615  lhpj1  35626  lhpmcvr4N  35630  lhpelim  35641  lhpmod2i2  35642  lhpmod6i1  35643  cdlemb2  35645  lhpat  35647  ltrnatb  35741  ltrnel  35743  ltrncnvel  35746  ltrncnv  35750  ltrnmwOLD  35756  trlval2  35768  trljat1  35771  trljat2  35772  trlnidatb  35782  cdlemc1  35796  cdlemc2  35797  cdlemc5  35800  cdlemc6  35801  cdleme0aa  35815  cdleme0b  35817  cdleme0c  35818  cdleme0e  35822  cdleme0fN  35823  cdleme01N  35826  cdleme0ex1N  35828  cdleme0moN  35830  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme4  35843  cdleme4a  35844  cdleme5  35845  cdleme8  35855  cdleme9  35858  cdleme10  35859  cdleme16aN  35864  cdleme11fN  35869  cdleme11g  35870  cdleme11k  35873  cdleme13  35877  cdleme17c  35893  cdleme17d1  35894  cdleme18c  35898  cdleme22gb  35899  cdlemeda  35903  cdlemednpq  35904  cdlemednuN  35905  cdleme19c  35910  cdleme20aN  35914  cdleme20bN  35915  cdleme20c  35916  cdleme22aa  35944  cdleme22d  35948  cdleme22e  35949  cdleme27cl  35971  cdleme27a  35972  cdleme30a  35983  cdleme42a  36076  cdleme42c  36077  cdlemg2fv2  36205  cdlemg2m  36209  cdlemg4g  36221  cdlemg4  36222  cdlemg6c  36225  cdlemg7aN  36230  cdlemg9a  36237  cdlemg9b  36238  cdlemg10c  36244  cdlemg12a  36248  cdlemg12b  36249  cdlemg17a  36266  cdlemg18b  36284  cdlemg18c  36285  trlcoabs2N  36327  trlcolem  36331  tendoco2  36373  tendoicl  36401  cdlemi1  36423  cdlemi2  36424  cdlemj3  36428  tendocan  36429  cdlemk3  36438  cdlemk4  36439  cdlemk5a  36440  cdlemk9  36444  cdlemk9bN  36445  cdlemk10  36448  cdlemk30  36499  cdlemk31  36501  cdlemk39  36521  cdlemkfid1N  36526  cdlemkfid2N  36528  cdlemk19ylem  36535  cdlemk19xlem  36547  cdlemk53b  36561  cdlemk53  36562  cdlemk55a  36564  cdlemk43N  36568  cdlemk19u1  36574  cdlemm10N  36724  cdlemn2  36801  cdlemn10  36812  dihjustlem  36822  dihord2cN  36827  dihvalcq2  36853  dihopelvalcpre  36854  dihord5b  36865  dihord6b  36866  dihmeetlem2N  36905  dihmeetbclemN  36910  dihmeetlem4preN  36912  dihmeetALTN  36933  dochshpncl  36990  dochsatshpb  37058  hdmapval3N  37447  hgmap11  37511  pellfundex  37767  congtr  37849  fzmaxdif  37865  isnumbasgrplem2  37991  idomsubgmo  38093  ntrclsk13  38686  restuni3  39615  unirnmapsn  39720  ssmapsn  39722  infnsuprnmpt  39779  upbdrech  39833  suplesup  39868  infleinf  39901  supxrunb3  39936  mullimc  40166  islptre  40169  mullimcf  40173  neglimc  40197  limsupmnfuzlem  40276  limsupre3lem  40282  limsupre3uzlem  40285  icccncfext  40418  dvmptfprod  40478  stoweidlem31  40566  opnvonmbllem2  41168  smflimsuplem7  41353  prmdvdsfmtnof1lem1  41821  domnmsuppn0  42475  mndpfsupp  42482  lincext3  42570
  Copyright terms: Public domain W3C validator