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

Theorem simprl1 1099
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simprl1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜑)

Proof of Theorem simprl1
StepHypRef Expression
1 simpl1 1057 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantl 481 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  pwfseqlem1  9359  pwfseqlem5  9364  icodiamlt  14022  issubc3  16332  pgpfac1lem5  18301  clscon  21043  txlly  21249  txnlly  21250  itg2add  23332  ftc1a  23604  f1otrg  25551  ax5seglem6  25614  axcontlem9  25652  axcontlem10  25653  extwwlkfablem2  26605  locfinref  29236  erdszelem7  30433  cvmlift2lem10  30548  btwnouttr2  31299  btwnconn1lem13  31376  broutsideof2  31399  mpaaeu  36739  dfsalgen2  39235  elwspths2spth  41171  digexp  42199
 Copyright terms: Public domain W3C validator