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

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

Proof of Theorem simprl2
StepHypRef Expression
1 simpl2 1063 . 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:  icodiamlt  14103  issubc3  16425  clsconn  21138  txlly  21344  txnlly  21345  itg2add  23427  ftc1a  23699  f1otrg  25646  ax5seglem6  25709  axcontlem9  25747  axcontlem10  25748  clwwlksf  26775  locfinref  29682  erdszelem7  30879  btwnconn1lem13  31840  dfsalgen2  39853
 Copyright terms: Public domain W3C validator