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

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

Proof of Theorem simprl2
StepHypRef Expression
1 simpl2 1058 . 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:  icodiamlt  14022  issubc3  16332  clscon  21043  txlly  21249  txnlly  21250  itg2add  23332  ftc1a  23604  f1otrg  25551  ax5seglem6  25614  axcontlem9  25652  axcontlem10  25653  clwwlkf  26322  usg2spot2nb  26592  locfinref  29236  erdszelem7  30433  btwnconn1lem13  31376  dfsalgen2  39235  clwwlksf  41222
 Copyright terms: Public domain W3C validator