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

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

Proof of Theorem simpr3l
StepHypRef Expression
1 simp3l 1087 . 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:  ax5seg  25752  axcont  25790  segconeq  31812  idinside  31886  btwnconn1lem10  31898  segletr  31916  cdlemc3  34999  cdlemc4  35000  cdleme1  35033  cdleme2  35034  cdleme3b  35035  cdleme3c  35036  cdleme3e  35038  cdleme27a  35174  stoweidlem56  39610
  Copyright terms: Public domain W3C validator