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

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

Proof of Theorem simprl1
StepHypRef Expression
1 simp1 1130 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antrl 766 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072 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 385  df-3an 1074 This theorem is referenced by:  pwfseqlem1  9664  pwfseqlem5  9669  icodiamlt  14365  issubc3  16702  pgpfac1lem5  18670  clsconn  21427  txlly  21633  txnlly  21634  itg2add  23717  ftc1a  23991  f1otrg  25942  ax5seglem6  26005  axcontlem9  26043  axcontlem10  26044  elwspths2spth  27081  wwlksext2clwwlk  27179  locfinref  30209  erdszelem7  31478  cvmlift2lem10  31593  noprefixmo  32146  nosupbnd2  32160  btwnouttr2  32427  btwnconn1lem13  32504  broutsideof2  32527  mpaaeu  38214  dfsalgen2  41054  digexp  42903
 Copyright terms: Public domain W3C validator