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

Theorem simpr2r 1234
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 773 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr2 1190 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  poxp2  8168  poxp3  8175  frrlem8  8318  ttrcltr  9756  ttrclss  9760  rnttrcl  9762  ttrclselem2  9766  oppccatid  17762  subccatid  17891  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  kerf1ghm  19265  gsmsymgreqlem1  19448  ax5seg  28953  3pthdlem1  30183  segconeq  36011  ifscgr  36045  brofs2  36078  brifs2  36079  idinside  36085  btwnconn1lem8  36095  btwnconn1lem11  36098  btwnconn1lem12  36099  segcon2  36106  seglecgr12im  36111  unbdqndv2  36512  lplnexllnN  39566  paddasslem9  39830  paddasslem15  39836  pmodlem2  39849  lhp2lt  40003  isthincd2  49086  mndtccatid  49184
  Copyright terms: Public domain W3C validator