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

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

Proof of Theorem simprl1
StepHypRef Expression
1 simpl1 1146 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantl 473 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  9561  pwfseqlem5  9566  icodiamlt  14262  issubc3  16599  pgpfac1lem5  18567  clsconn  21324  txlly  21530  txnlly  21531  itg2add  23614  ftc1a  23888  f1otrg  25839  ax5seglem6  25902  axcontlem9  25940  axcontlem10  25941  elwspths2spth  26978  wwlksext2clwwlk  27076  locfinref  30106  erdszelem7  31375  cvmlift2lem10  31490  noprefixmo  32043  nosupbnd2  32057  btwnouttr2  32324  btwnconn1lem13  32401  broutsideof2  32424  mpaaeu  38107  dfsalgen2  40947  digexp  42796
  Copyright terms: Public domain W3C validator