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

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

Proof of Theorem simpr2r
StepHypRef Expression
1 simprr 756 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr2 1204 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:  oppccatid  16586  subccatid  16713  setccatid  16941  catccatid  16959  estrccatid  16979  xpccatid  17036  gsmsymgreqlem1  18057  kerf1hrm  18953  ax5seg  26039  3pthdlem1  27344  frrlem11  32129  segconeq  32454  ifscgr  32488  brofs2  32521  brifs2  32522  idinside  32528  btwnconn1lem8  32538  btwnconn1lem11  32541  btwnconn1lem12  32542  segcon2  32549  seglecgr12im  32554  unbdqndv2  32839  lplnexllnN  35372  paddasslem9  35636  paddasslem15  35642  pmodlem2  35655  lhp2lt  35809
  Copyright terms: Public domain W3C validator