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

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

Proof of Theorem simp2ll
StepHypRef Expression
1 simpll 774 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant2 1157 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  tfrlem5  7712  omeu  7902  4sqlem18  15883  vdwlem10  15911  0catg  16552  mvrf1  19634  mdetuni0  20638  mdetmul  20640  tsmsxp  22171  ax5seglem3  26025  btwnconn1lem1  32515  btwnconn1lem2  32516  btwnconn1lem3  32517  btwnconn1lem12  32526  btwnconn1lem13  32527  lshpkrlem6  34895  athgt  35236  2llnjN  35347  dalaw  35666  lhpmcvr4N  35806  cdlemb2  35821  4atexlemex6  35854  cdlemd7  35985  cdleme01N  36002  cdleme02N  36003  cdleme0ex1N  36004  cdleme0ex2N  36005  cdleme7aa  36023  cdleme7c  36026  cdleme7d  36027  cdleme7e  36028  cdleme7ga  36029  cdleme7  36030  cdleme11a  36041  cdleme20k  36100  cdleme27cl  36147  cdleme42e  36260  cdleme42h  36263  cdleme42i  36264  cdlemf  36344  cdlemg2kq  36383  cdlemg2m  36385  cdlemg8a  36408  cdlemg11aq  36419  cdlemg10c  36420  cdlemg11b  36423  cdlemg17a  36442  cdlemg31b0N  36475  cdlemg31c  36480  cdlemg33c0  36483  cdlemg41  36499  cdlemh2  36597  cdlemn9  36986  dihglbcpreN  37081  dihmeetlem3N  37086  dihmeetlem13N  37100  pellex  37901  expmordi  38013
  Copyright terms: Public domain W3C validator