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

Theorem simprl1 1282
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 1167 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antrl 720 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  pwfseqlem1  9768  pwfseqlem5  9773  icodiamlt  14515  issubc3  16823  pgpfac1lem5  18794  clsconn  21562  txlly  21768  txnlly  21769  itg2add  23867  ftc1a  24141  f1otrg  26108  ax5seglem6  26171  axcontlem9  26209  axcontlem10  26210  elwspths2spth  27258  wwlksext2clwwlk  27373  locfinref  30424  erdszelem7  31696  cvmlift2lem10  31811  noprefixmo  32361  nosupbnd2  32375  btwnouttr2  32642  btwnconn1lem13  32719  broutsideof2  32742  mpaaeu  38505  dfsalgen2  41302  digexp  43200
  Copyright terms: Public domain W3C validator