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

Theorem simpl1r 1222
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpl1r ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpl1r
StepHypRef Expression
1 simplr 768 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl1 1182 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  soisores  7073  tfisi  7567  omopth2  8206  swrdsbslen  14026  swrdspsleq  14027  repswswrd  14146  ramub1lem1  16360  efgsfo  18865  lbspss  19854  maducoeval2  21249  madurid  21253  decpmatmullem  21379  mp2pm2mplem4  21417  llyrest  22093  ptbasin  22185  basqtop  22319  ustuqtop1  22850  mulcxp  25279  elwwlks2ons3im  27743  br8d  30372  isarchi2  30846  archiabllem2c  30856  cvmlift2lem10  32616  5segofs  33524  btwnconn1lem13  33617  2llnjaN  36807  paddasslem12  37072  lhp2lt  37242  lhpexle2lem  37250  lhpmcvr3  37266  lhpat3  37287  trlval3  37428  cdleme17b  37528  cdlemefr27cl  37644  cdlemg11b  37883  tendococl  38013  cdlemj3  38064  cdlemk35s-id  38179  cdlemk39s-id  38181  cdlemk53b  38197  cdlemk35u  38205  cdlemm10N  38359  dihopelvalcpre  38489  dihord6apre  38497  dihord5b  38500  dihglblem5apreN  38532  dihglblem2N  38535  dihmeetlem6  38550  dihmeetlem18N  38565  dvh3dim2  38689  dvh3dim3N  38690  jm2.25lem1  39855  limcleqr  42212  icccncfext  42455  fourierdlem87  42761  sge0seq  43011  smflimsuplem7  43383  itscnhlc0xyqsol  45105  itscnhlinecirc02plem2  45123
  Copyright terms: Public domain W3C validator