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

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

Proof of Theorem simprl2
StepHypRef Expression
1 simp2 1131 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antrl 699 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  icodiamlt  14381  issubc3  16715  clsconn  21453  txlly  21659  txnlly  21660  itg2add  23745  ftc1a  24019  f1otrg  25971  ax5seglem6  26034  axcontlem9  26072  axcontlem10  26073  clwwlkf  27202  locfinref  30245  erdszelem7  31514  noprefixmo  32182  nosupbnd2  32196  btwnconn1lem13  32540  dfsalgen2  41072
  Copyright terms: Public domain W3C validator