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

Theorem simpl2r 1227
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 767 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl2 1186 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  soisores  7268  omopth2  8527  ttrcltr  9648  fin23lem11  10249  xmulasslem3  13197  ssfzo12bi  13659  ntrivcvgmul  15779  pockthg  16770  gsumsgrpccat  18642  efgred  19521  lspfixed  20574  decpmatmullem  22104  decpmatmul  22105  unconn  22764  llyrest  22820  basqtop  23046  tmdgsum  23430  tsmsxp  23490  ucncn  23621  mulcxp  26024  cxple2  26036  nogt01o  27028  noetalem1  27073  cofcut1  27223  ax5seglem1  27763  ax5seglem2  27764  axpasch  27776  axcontlem4  27802  1pthon2v  28983  cvmlift2lem10  33775  br4  34201  cgrcomim  34541  btwnintr  34571  btwnouttr2  34574  btwndiff  34579  btwnconn1lem14  34652  btwnconn3  34655  segcon2  34657  brsegle  34660  brsegle2  34661  segleantisym  34667  outsideofeu  34683  eqlkr  37528  eqlkr2  37529  lkrlsp  37531  atbtwn  37876  3dimlem3OLDN  37892  3dim3  37899  3atlem7  37919  4atlem0a  38023  4atlem3a  38027  4atlem11  38039  lneq2at  38208  lnatexN  38209  paddasslem6  38255  llnexchb2  38299  lhpexle2lem  38439  lhpexle3  38442  lhp2at0nle  38465  lhpat3  38476  trlnid  38609  ltrneq3  38638  cdleme17b  38717  cdleme27cl  38796  cdlemefrs29bpre0  38826  cdlemefrs29clN  38829  cdlemefrs32fva  38830  cdlemefs32sn1aw  38844  cdleme32le  38877  ltrniotavalbN  39014  cdlemg6  39053  cdlemg7N  39056  cdlemg11b  39072  cdlemg15a  39085  cdlemg15  39086  cdlemg39  39146  trlcone  39158  cdlemg42  39159  tendoconid  39259  tendotr  39260  cdlemk39u  39398  cdlemk19u  39400  tendoex  39405  cdlemm10N  39548  dihord2pre  39655  dihord4  39688  dihord5b  39689  dihglbcpreN  39730  dihmeetlem13N  39749  dih1dimatlem0  39758  mzpcong  41234  jm2.25lem1  41260  jm2.26  41264  idomsubgmo  41463  itscnhlinecirc02plem2  46801
  Copyright terms: Public domain W3C validator