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

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

Proof of Theorem simpl2r
StepHypRef Expression
1 simplr 768 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl2 1183 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  7063  omopth2  8197  fin23lem11  9732  xmulasslem3  12671  ssfzo12bi  13131  ntrivcvgmul  15253  pockthg  16235  gsumsgrpccat  17999  efgred  18869  lspfixed  19896  decpmatmullem  21379  decpmatmul  21380  unconn  22037  llyrest  22093  basqtop  22319  tmdgsum  22703  tsmsxp  22763  ucncn  22894  mulcxp  25279  cxple2  25291  ax5seglem1  26725  ax5seglem2  26726  axpasch  26738  axcontlem4  26764  1pthon2v  27941  cvmlift2lem10  32667  br4  33102  cgrcomim  33558  btwnintr  33588  btwnouttr2  33591  btwndiff  33596  btwnconn1lem14  33669  btwnconn3  33672  segcon2  33674  brsegle  33677  brsegle2  33678  segleantisym  33684  outsideofeu  33700  eqlkr  36388  eqlkr2  36389  lkrlsp  36391  atbtwn  36735  3dimlem3OLDN  36751  3dim3  36758  3atlem7  36778  4atlem0a  36882  4atlem3a  36886  4atlem11  36898  lneq2at  37067  lnatexN  37068  paddasslem6  37114  llnexchb2  37158  lhpexle2lem  37298  lhpexle3  37301  lhp2at0nle  37324  lhpat3  37335  trlnid  37468  ltrneq3  37497  cdleme17b  37576  cdleme27cl  37655  cdlemefrs29bpre0  37685  cdlemefrs29clN  37688  cdlemefrs32fva  37689  cdlemefs32sn1aw  37703  cdleme32le  37736  ltrniotavalbN  37873  cdlemg6  37912  cdlemg7N  37915  cdlemg11b  37931  cdlemg15a  37944  cdlemg15  37945  cdlemg39  38005  trlcone  38017  cdlemg42  38018  tendoconid  38118  tendotr  38119  cdlemk39u  38257  cdlemk19u  38259  tendoex  38264  cdlemm10N  38407  dihord2pre  38514  dihord4  38547  dihord5b  38548  dihglbcpreN  38589  dihmeetlem13N  38608  dih1dimatlem0  38617  mzpcong  39900  jm2.25lem1  39926  jm2.26  39930  idomsubgmo  40129  itscnhlinecirc02plem2  45184
  Copyright terms: Public domain W3C validator