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

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

Proof of Theorem simpr3l
StepHypRef Expression
1 simprl 789 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr3 1247 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  ax5seg  26237  axcont  26275  nosupbnd1lem5  32397  segconeq  32656  idinside  32730  btwnconn1lem10  32742  segletr  32760  cdlemc3  36268  cdlemc4  36269  cdleme1  36302  cdleme2  36303  cdleme3b  36304  cdleme3c  36305  cdleme3e  36307  cdleme27a  36442  stoweidlem56  41067
  Copyright terms: Public domain W3C validator