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

Theorem simpr3l 1299
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 811 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr3 1206 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  ax5seg  26038  axcont  26076  nosupbnd1lem5  32185  segconeq  32444  idinside  32518  btwnconn1lem10  32530  segletr  32548  cdlemc3  36001  cdlemc4  36002  cdleme1  36035  cdleme2  36036  cdleme3b  36037  cdleme3c  36038  cdleme3e  36040  cdleme27a  36175  stoweidlem56  40794
  Copyright terms: Public domain W3C validator