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

Theorem simprl3 1220
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 1138 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antrl 726 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  poxp3  8138  ttrcltr  9713  pwfseqlem5  10660  icodiamlt  15386  issubc3  17803  pgpfac1lem5  19990  clsconn  23154  txlly  23360  txnlly  23361  itg2add  25501  ftc1a  25778  nosupprefixmo  27427  noinfprefixmo  27428  nosupbnd2  27443  noinfbnd2  27458  mulsprop  27813  f1otrg  28377  ax5seglem6  28447  axcontlem10  28486  numclwwlk5  29896  locfinref  33107  btwnouttr2  35286  btwnconn1lem13  35363  midofsegid  35368  outsideofeq  35394  ivthALT  35523  mpaaeu  42194  dfsalgen2  45356
  Copyright terms: Public domain W3C validator