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

Theorem simpl2r 1284
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 744 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl2 1201 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  soisores  6720  omopth2  7818  fin23lem11  9341  xmulasslem3  12321  ssfzo12bi  12771  ntrivcvgmul  14841  pockthg  15817  gsmsymgreqlem2  18058  efgred  18368  lspfixed  19341  lspfixedOLD  19342  decpmatmullem  20796  decpmatmul  20797  unconn  21453  llyrest  21509  basqtop  21735  tmdgsum  22119  tsmsxp  22178  ucncn  22309  mulcxp  24652  cxple2  24664  ax5seglem1  26029  ax5seglem2  26030  axpasch  26042  axcontlem4  26068  1pthon2v  27333  cvmlift2lem10  31632  br4  31986  cgrcomim  32433  btwnintr  32463  btwnouttr2  32466  btwndiff  32471  btwnconn1lem14  32544  btwnconn3  32547  segcon2  32549  brsegle  32552  brsegle2  32553  segleantisym  32559  outsideofeu  32575  eqlkr  34908  eqlkr2  34909  lkrlsp  34911  atbtwn  35254  3dimlem3OLDN  35270  3dim3  35277  3atlem7  35297  4atlem0a  35401  4atlem3a  35405  4atlem11  35417  lneq2at  35586  lnatexN  35587  paddasslem6  35633  llnexchb2  35677  lhpexle2lem  35817  lhpexle3  35820  lhp2at0nle  35843  lhpat3  35854  trlnid  35988  ltrneq3  36017  cdleme17b  36096  cdleme27cl  36175  cdlemefrs29bpre0  36205  cdlemefrs29clN  36208  cdlemefrs32fva  36209  cdlemefs32sn1aw  36223  cdleme32le  36256  ltrniotavalbN  36393  cdlemg6  36432  cdlemg7N  36435  cdlemg11b  36451  cdlemg15a  36464  cdlemg15  36465  cdlemg39  36525  trlcone  36537  cdlemg42  36538  tendoconid  36638  tendotr  36639  cdlemk39u  36777  cdlemk19u  36779  tendoex  36784  cdlemm10N  36928  dihord2pre  37035  dihord4  37068  dihord5b  37069  dihglbcpreN  37110  dihmeetlem13N  37129  dih1dimatlem0  37138  mzpcong  38065  jm2.25lem1  38091  jm2.26  38095  idomsubgmo  38302
  Copyright terms: Public domain W3C validator