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

Theorem simpr3l 1270
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 761 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr3 1198 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 1073
This theorem is referenced by:  ax5seg  26287  axcont  26325  nosupbnd1lem5  32447  segconeq  32706  idinside  32780  btwnconn1lem10  32792  segletr  32810  cdlemc3  36347  cdlemc4  36348  cdleme1  36381  cdleme2  36382  cdleme3b  36383  cdleme3c  36384  cdleme3e  36386  cdleme27a  36521  stoweidlem56  41200
  Copyright terms: Public domain W3C validator