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

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

Proof of Theorem simprl1
StepHypRef Expression
1 simpl1 1062 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantl 482 1 ((𝜏 ∧ ((𝜑𝜓𝜒) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  pwfseqlem1  9425  pwfseqlem5  9430  icodiamlt  14103  issubc3  16425  pgpfac1lem5  18394  clsconn  21138  txlly  21344  txnlly  21345  itg2add  23427  ftc1a  23699  f1otrg  25646  ax5seglem6  25709  axcontlem9  25747  axcontlem10  25748  elwspths2spth  26723  locfinref  29682  erdszelem7  30879  cvmlift2lem10  30994  btwnouttr2  31763  btwnconn1lem13  31840  broutsideof2  31863  mpaaeu  37187  dfsalgen2  39853  digexp  41667
  Copyright terms: Public domain W3C validator