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

Theorem simpr2r 1233
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 771 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr2 1189 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:  poxp2  8074  poxp3  8081  frrlem8  8223  ttrcltr  9651  ttrclss  9655  rnttrcl  9657  ttrclselem2  9661  oppccatid  17600  subccatid  17731  setccatid  17969  catccatid  17991  estrccatid  18018  xpccatid  18075  gsmsymgreqlem1  19210  kerf1ghm  20175  ax5seg  27885  3pthdlem1  29106  segconeq  34586  ifscgr  34620  brofs2  34653  brifs2  34654  idinside  34660  btwnconn1lem8  34670  btwnconn1lem11  34673  btwnconn1lem12  34674  segcon2  34681  seglecgr12im  34686  unbdqndv2  34965  lplnexllnN  38018  paddasslem9  38282  paddasslem15  38288  pmodlem2  38301  lhp2lt  38455  isthincd2  47030  mndtccatid  47085
  Copyright terms: Public domain W3C validator