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

Theorem simpr3l 1231
 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 770 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr3 1187 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  ax5seg  26730  axcont  26768  nosupbnd1lem5  33286  segconeq  33545  idinside  33619  btwnconn1lem10  33631  segletr  33649  cdlemc3  37448  cdlemc4  37449  cdleme1  37482  cdleme2  37483  cdleme3b  37484  cdleme3c  37485  cdleme3e  37487  cdleme27a  37622  stoweidlem56  42638
 Copyright terms: Public domain W3C validator