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

Theorem simprl2 1211
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 1129 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antrl 724 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  icodiamlt  14783  issubc3  17107  clsconn  21966  txlly  22172  txnlly  22173  itg2add  24287  ftc1a  24561  f1otrg  26584  ax5seglem6  26647  axcontlem9  26685  axcontlem10  26686  clwwlkf  27753  locfinref  31004  erdszelem7  32341  noprefixmo  33099  nosupbnd2  33113  btwnconn1lem13  33457  dfsalgen2  42501
  Copyright terms: Public domain W3C validator