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

Theorem simpl2r 1135
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl2r (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpl2r
StepHypRef Expression
1 simp2r 1108 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
21adantr 480 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  soisores  6617  omopth2  7709  fin23lem11  9177  xmulasslem3  12154  ssfzo12bi  12603  ntrivcvgmul  14678  pockthg  15657  gsmsymgreqlem2  17897  efgred  18207  lspfixed  19176  decpmatmullem  20624  decpmatmul  20625  unconn  21280  llyrest  21336  basqtop  21562  tmdgsum  21946  tsmsxp  22005  ucncn  22136  mulcxp  24476  cxple2  24488  ax5seglem1  25853  ax5seglem2  25854  axpasch  25866  axcontlem4  25892  1pthon2v  27131  cvmlift2lem10  31420  br4  31774  cgrcomim  32221  btwnintr  32251  btwnouttr2  32254  btwndiff  32259  btwnconn1lem14  32332  btwnconn3  32335  segcon2  32337  brsegle  32340  brsegle2  32341  segleantisym  32347  outsideofeu  32363  eqlkr  34704  eqlkr2  34705  lkrlsp  34707  atbtwn  35050  3dimlem3OLDN  35066  3dim3  35073  3atlem7  35093  4atlem0a  35197  4atlem3a  35201  4atlem11  35213  lneq2at  35382  lnatexN  35383  paddasslem6  35429  llnexchb2  35473  lhpexle2lem  35613  lhpexle3  35616  lhp2at0nle  35639  lhpat3  35650  trlnid  35784  ltrneq3  35813  cdleme17b  35892  cdleme27cl  35971  cdlemefrs29bpre0  36001  cdlemefrs29clN  36004  cdlemefrs32fva  36005  cdlemefs32sn1aw  36019  cdleme32le  36052  ltrniotavalbN  36189  cdlemg6  36228  cdlemg7N  36231  cdlemg11b  36247  cdlemg15a  36260  cdlemg15  36261  cdlemg39  36321  trlcone  36333  cdlemg42  36334  tendoconid  36434  tendotr  36435  cdlemk39u  36573  cdlemk19u  36575  tendoex  36580  cdlemm10N  36724  dihord2pre  36831  dihord4  36864  dihord5b  36865  dihglbcpreN  36906  dihmeetlem13N  36925  dih1dimatlem0  36934  mzpcong  37856  jm2.25lem1  37882  jm2.26  37886  idomsubgmo  38093
  Copyright terms: Public domain W3C validator