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

Theorem simprl3 1217
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simprl3 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprl3
StepHypRef Expression
1 simp3 1135 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antrl 727 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:  pwfseqlem5  10136  icodiamlt  14856  issubc3  17191  pgpfac1lem5  19282  clsconn  22143  txlly  22349  txnlly  22350  itg2add  24472  ftc1a  24749  f1otrg  26777  ax5seglem6  26840  axcontlem10  26879  numclwwlk5  28285  locfinref  31324  nosupprefixmo  33500  noinfprefixmo  33501  nosupbnd2  33516  noinfbnd2  33531  btwnouttr2  33907  btwnconn1lem13  33984  midofsegid  33989  outsideofeq  34015  ivthALT  34107  mpaaeu  40502  dfsalgen2  43382
 Copyright terms: Public domain W3C validator