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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 475 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1074 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simpl1r  1105  simpr1r  1111  simp11r  1165  simp21r  1171  simp31r  1177  vtoclgftOLD  3223  funprgOLD  5837  omeulem2  7523  uniinqs  7687  unxpdomlem3  8024  elfiun  8192  cofsmo  8947  isfin2-2  8997  isf32lem9  9039  tskun  9460  tskurn  9463  reclem3pr  9723  dedekind  10047  dmdcan  10580  lt2msq1  10752  supmullem1  10836  supmul  10838  xaddass2  11905  xlt2add  11915  xmulasslem3  11941  iccsplit  12128  expaddzlem  12716  expaddz  12717  expmulz  12719  limsupgle  13998  o1add  14134  o1mul  14135  o1sub  14136  bitsfzo  14937  sadfval  14954  smufval  14979  prmexpb  15210  4sqlem18  15446  vdwlem10  15474  mrieqv2d  16064  curf1  16630  mndodcong  17726  subgabl  18006  gex2abl  18019  cntzsubr  18577  abvres  18604  lbsind2  18844  lbsextlem2  18922  lbsextg  18925  matring  20006  mdetunilem8  20182  maducoeval  20202  maducoeval2  20203  madurid  20207  cramerimplem3  20248  pmatcollpw2  20340  pm2mpf1  20361  cnprest  20841  isreg2  20929  fbssfi  21389  hausflimlem  21531  tmdgsum  21647  ssblps  21974  ssbl  21975  xrsmopn  22351  dvres2  23395  vieta1  23784  aalioulem4  23807  efgh  24004  cxpadd  24138  cxpsub  24141  divcxp  24146  cxple2  24156  cxplt2  24157  cxpcn3lem  24201  angcan  24245  ang180lem5  24256  isosctrlem3  24263  lgssq  24775  brbtwn2  25499  axcontlem4  25561  axcontlem8  25565  clwwlknimp  26066  chscllem4  27685  ogrpinvlt  28857  pstmval  29068  measinblem  29412  cvmlift2lem6  30346  poseq  30796  linethru  31232  cnres2  32531  lcv1  33145  lfl1  33174  lshpkrex  33222  hlrelat3  33515  cvrval3  33516  cvrval4N  33517  athgt  33559  atcvrlln2  33622  atcvrlln  33623  lvolnle3at  33685  lvolnlelpln  33688  4atlem11  33712  4atlem12  33715  2lplnj  33723  dalemddea  33787  cdlema2N  33895  paddasslem2  33924  atmod1i1m  33961  lhp2lt  34104  lhp0lt  34106  lhpexle3lem  34114  lhpj1  34125  lhpmcvr4N  34129  lhpelim  34140  lhpmod2i2  34141  lhpmod6i1  34142  cdlemb2  34144  lhpat  34146  ltrnatb  34240  ltrnel  34242  ltrncnvel  34245  ltrncnv  34249  ltrnmwOLD  34255  trlval2  34267  trljat1  34270  trljat2  34271  trlnidatb  34281  cdlemc1  34295  cdlemc2  34296  cdlemc5  34299  cdlemc6  34300  cdleme0aa  34314  cdleme0b  34316  cdleme0c  34317  cdleme0e  34321  cdleme0fN  34322  cdleme01N  34325  cdleme0ex1N  34327  cdleme0moN  34329  cdleme3g  34338  cdleme3h  34339  cdleme3  34341  cdleme4  34342  cdleme4a  34343  cdleme5  34344  cdleme8  34354  cdleme9  34357  cdleme10  34358  cdleme16aN  34363  cdleme11fN  34368  cdleme11g  34369  cdleme11k  34372  cdleme13  34376  cdleme17c  34392  cdleme17d1  34393  cdleme18c  34397  cdleme22gb  34398  cdlemeda  34402  cdlemednpq  34403  cdlemednuN  34404  cdleme19c  34410  cdleme20aN  34414  cdleme20bN  34415  cdleme20c  34416  cdleme22aa  34444  cdleme22d  34448  cdleme22e  34449  cdleme27cl  34471  cdleme27a  34472  cdleme30a  34483  cdleme42a  34576  cdleme42c  34577  cdlemg2fv2  34705  cdlemg2m  34709  cdlemg4g  34721  cdlemg4  34722  cdlemg6c  34725  cdlemg7aN  34730  cdlemg9a  34737  cdlemg9b  34738  cdlemg10c  34744  cdlemg12a  34748  cdlemg12b  34749  cdlemg17a  34766  cdlemg18b  34784  cdlemg18c  34785  trlcoabs2N  34827  trlcolem  34831  tendoco2  34873  tendoicl  34901  cdlemi1  34923  cdlemi2  34924  cdlemj3  34928  tendocan  34929  cdlemk3  34938  cdlemk4  34939  cdlemk5a  34940  cdlemk9  34944  cdlemk9bN  34945  cdlemk10  34948  cdlemk30  34999  cdlemk31  35001  cdlemk39  35021  cdlemkfid1N  35026  cdlemkfid2N  35028  cdlemk19ylem  35035  cdlemk19xlem  35047  cdlemk53b  35061  cdlemk53  35062  cdlemk55a  35064  cdlemk43N  35068  cdlemk19u1  35074  cdlemm10N  35224  cdlemn2  35301  cdlemn10  35312  dihjustlem  35322  dihord2cN  35327  dihvalcq2  35353  dihopelvalcpre  35354  dihord5b  35365  dihord6b  35366  dihmeetlem2N  35405  dihmeetbclemN  35410  dihmeetlem4preN  35412  dihmeetALTN  35433  dochshpncl  35490  dochsatshpb  35558  hdmapval3N  35947  hgmap11  36011  pellfundex  36267  congtr  36349  fzmaxdif  36365  isnumbasgrplem2  36492  idomsubgmo  36594  ntrclsk13  37188  restuni3  38132  unirnmapsn  38200  ssmapsn  38202  upbdrech  38259  suplesup  38296  infleinf  38329  mullimc  38483  islptre  38486  mullimcf  38490  neglimc  38514  icccncfext  38573  dvmptfprod  38635  stoweidlem31  38724  opnvonmbllem2  39323  prmdvdsfmtnof1lem1  39835  uhgr2edg  40433  domnmsuppn0  41942  mndpfsupp  41949  lincext3  42037
  Copyright terms: Public domain W3C validator