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

Theorem simprl2 1216
 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 1134 . 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:  icodiamlt  14848  issubc3  17183  clsconn  22135  txlly  22341  txnlly  22342  itg2add  24464  ftc1a  24741  f1otrg  26769  ax5seglem6  26832  axcontlem9  26870  axcontlem10  26871  clwwlkf  27936  locfinref  31316  erdszelem7  32679  poxp2  33349  nosupprefixmo  33492  noinfprefixmo  33493  nosupbnd2  33508  noinfbnd2  33523  btwnconn1lem13  33976  dfsalgen2  43375
 Copyright terms: Public domain W3C validator