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

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

Proof of Theorem simpr2r
StepHypRef Expression
1 simp2r 1086 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
21adantl 482 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  oppccatid  16300  subccatid  16427  setccatid  16655  catccatid  16673  estrccatid  16693  xpccatid  16749  gsmsymgreqlem1  17771  kerf1hrm  18664  ax5seg  25718  3pthdlem1  26890  segconeq  31759  ifscgr  31793  brofs2  31826  brifs2  31827  idinside  31833  btwnconn1lem8  31843  btwnconn1lem11  31846  btwnconn1lem12  31847  segcon2  31854  seglecgr12im  31859  unbdqndv2  32144  lplnexllnN  34330  paddasslem9  34594  paddasslem15  34600  pmodlem2  34613  lhp2lt  34767
  Copyright terms: Public domain W3C validator