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

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

Proof of Theorem simpl2l
StepHypRef Expression
1 simp2l 1085 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
21adantr 481 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:  soisores  6537  omopth2  7616  fin23lem11  9090  dedekind  10151  xaddass  12029  swrdsbslen  13393  ntrivcvgmul  14566  pockthg  15541  gsmsymgreqlem2  17779  efgred  18089  decpmatmullem  20504  decpmatmul  20505  unconn  21151  basqtop  21433  utop2nei  21973  ucncn  22008  cxple2  24356  cxple2a  24358  ax5seglem1  25721  ax5seglem2  25722  axpasch  25734  axcontlem4  25760  1pthon2v  26892  cvmlift2lem10  31029  br4  31383  noprefixmo  31600  cgrcomim  31765  btwnintr  31795  btwnouttr2  31798  btwndiff  31803  btwnconn1lem14  31876  btwnconn3  31879  segcon2  31881  brsegle  31884  brsegle2  31885  segleantisym  31891  seglelin  31892  outsideofeu  31907  eqlkr  33893  eqlkr2  33894  lkrlsp  33896  atbtwn  34239  athgt  34249  3dimlem3  34254  3dimlem3OLDN  34255  3dim3  34262  3atlem7  34282  4atlem0a  34386  4atlem3a  34390  4atlem11  34402  lneq2at  34571  lnatexN  34572  cdlemb  34587  paddasslem6  34618  llnexchb2  34662  lhp2lt  34794  lhpexle2lem  34802  lhpexle3  34805  lhpmcvr3  34818  lhpat3  34839  ltrnnidn  34968  ltrneq3  35002  cdleme17b  35081  cdleme25a  35148  cdleme25dN  35151  cdleme27cl  35161  cdlemefrs29bpre0  35191  cdlemefs32sn1aw  35209  cdleme32le  35242  cdleme46f2g2  35288  cdleme46f2g1  35289  cdleme50trn3  35348  trlord  35364  ltrniotavalbN  35379  cdlemg6  35418  cdlemg7N  35421  cdlemg11b  35437  cdlemg15a  35450  cdlemg15  35451  cdlemg39  35511  trlcone  35523  cdlemg42  35524  tendoconid  35624  tendotr  35625  cdlemk39u  35763  cdlemk19u  35765  cdleml5N  35775  cdlemm10N  35914  dihord11b  36018  dihord2pre  36021  dihvalcqpre  36031  dihopelvalcpre  36044  dihord6apre  36052  dihord4  36054  dihord5b  36055  dihglblem5apreN  36087  dihmeetlem13N  36115  dihmeetlem19N  36121  dih1dimatlem0  36124  qirropth  36980  mzpcong  37046  jm2.25lem1  37072  jm2.26  37076  idomsubgmo  37284  fourierdlem42  39694  fourierdlem97  39748
  Copyright terms: Public domain W3C validator