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

Theorem simprl2 1220
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 1138 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antrl 727 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  poxp2  8124  poxp3  8131  icodiamlt  15378  issubc3  17795  clsconn  22916  txlly  23122  txnlly  23123  itg2add  25259  ftc1a  25536  nosupprefixmo  27183  noinfprefixmo  27184  nosupbnd2  27199  noinfbnd2  27214  mulsprop  27566  f1otrg  28102  ax5seglem6  28172  axcontlem9  28210  axcontlem10  28211  clwwlkf  29280  locfinref  32759  erdszelem7  34126  btwnconn1lem13  35009  dfsalgen2  44992
  Copyright terms: Public domain W3C validator