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

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

Proof of Theorem simpl1l
StepHypRef Expression
1 simp1l 1083 . 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  6532  tfisi  7006  omopth2  7610  swrdsbslen  13381  swrdspsleq  13382  repswswrd  13463  ramub1lem1  15649  cntzsubr  18728  lbspss  18996  maducoeval2  20360  cramer  20411  neiptopnei  20841  ptbasin  21285  basqtop  21419  tmdgsum  21804  ustuqtop1  21950  cxplea  24337  cxple2  24338  ewlkle  26365  uspgr2wlkeq2  26406  extwwlkfablem2  27062  br8d  29256  isarchi2  29516  archiabllem2c  29526  cvmlift2lem10  30994  5segofs  31747  2llnjaN  34318  lvolnle3at  34334  paddasslem12  34583  paddasslem13  34584  atmod1i1m  34610  lhp2lt  34753  lhpexle2lem  34761  lhpmcvr3  34777  lhpat3  34798  ltrneq2  34900  trlnle  34939  trlval3  34940  trlval4  34941  cdleme0moN  34978  cdleme17b  35040  cdlemefrs29pre00  35149  cdlemefr27cl  35157  cdleme42ke  35239  cdleme42mgN  35242  cdleme46f2g2  35247  cdleme46f2g1  35248  cdleme50eq  35295  cdleme50trn3  35307  trlord  35323  cdlemg6c  35374  cdlemg11b  35396  cdlemg18a  35432  cdlemg42  35483  cdlemg46  35489  trljco  35494  tendococl  35526  cdlemj3  35577  tendotr  35584  cdlemk35s-id  35692  cdlemk39s-id  35694  cdlemk53b  35710  cdlemk53  35711  cdlemk35u  35718  tendoex  35729  cdlemm10N  35873  dihopelvalcpre  36003  dihord6apre  36011  dihord5b  36014  dihglblem5apreN  36046  dihglblem2N  36049  dihmeetlem4preN  36061  dihmeetlem6  36064  dihmeetlem10N  36071  dihmeetlem11N  36072  dihmeetlem16N  36077  dihmeetlem17N  36078  dihmeetlem18N  36079  dihmeetlem19N  36080  dihmeetALTN  36082  dihlspsnat  36088  dvh3dim2  36203  dvh3dim3N  36204  jm2.25lem1  37031  jm2.26  37035  limcperiod  39251  0ellimcdiv  39272  cncfshift  39377  cncfperiod  39382  icccncfext  39391  stoweidlem34  39545  fourierdlem48  39665  fourierdlem87  39704  sge0xaddlem2  39945  smflimsuplem7  40326  domnmsuppn0  41412
  Copyright terms: Public domain W3C validator