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

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

Proof of Theorem simprl3
StepHypRef Expression
1 simpl3 1064 . 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:  pwfseqlem5  9429  icodiamlt  14108  issubc3  16430  pgpfac1lem5  18399  clsconn  21143  txlly  21349  txnlly  21350  itg2add  23432  ftc1a  23704  f1otrg  25651  ax5seglem6  25714  axcontlem10  25753  numclwwlk5  27100  locfinref  29690  btwnouttr2  31771  btwnconn1lem13  31848  midofsegid  31853  outsideofeq  31879  ivthALT  31972  mpaaeu  37201  dfsalgen2  39866
 Copyright terms: Public domain W3C validator