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

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

Proof of Theorem simpr3l
StepHypRef Expression
1 simp3l 1082 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
21adantl 481 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  ax5seg  25618  axcont  25656  segconeq  31287  idinside  31361  btwnconn1lem10  31373  segletr  31391  cdlemc3  34498  cdlemc4  34499  cdleme1  34532  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme3e  34537  cdleme27a  34673  stoweidlem56  38949
 Copyright terms: Public domain W3C validator