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

Theorem simprl1 1215
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 1133 . 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:  pwfseqlem1  10074  pwfseqlem5  10079  icodiamlt  14793  issubc3  17117  pgpfac1lem5  19199  clsconn  22033  txlly  22239  txnlly  22240  itg2add  24361  ftc1a  24638  f1otrg  26663  ax5seglem6  26726  axcontlem9  26764  axcontlem10  26765  elwspths2spth  27751  wwlksext2clwwlk  27840  locfinref  31135  erdszelem7  32471  cvmlift2lem10  32586  noprefixmo  33229  nosupbnd2  33243  btwnouttr2  33510  btwnconn1lem13  33587  broutsideof2  33610  mpaaeu  39950  dfsalgen2  42847  fundcmpsurinjpreimafv  43791  digexp  44886  line2xlem  45021
  Copyright terms: Public domain W3C validator