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

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

Proof of Theorem simpl1l
StepHypRef Expression
1 simp1l 1158 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
21adantr 472 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:  soisores  6660  tfisi  7143  omopth2  7752  swrdsbslen  13537  swrdspsleq  13538  repswswrd  13620  ramub1lem1  15821  cntzsubr  18903  lbspss  19173  maducoeval2  20537  cramer  20588  neiptopnei  21027  ptbasin  21471  basqtop  21605  tmdgsum  21989  ustuqtop1  22135  cxplea  24530  cxple2  24531  ewlkle  26600  uspgr2wlkeq2  26642  br8d  29618  isarchi2  29937  archiabllem2c  29947  cvmlift2lem10  31490  nosupbnd2lem1  32056  5segofs  32308  2llnjaN  35240  lvolnle3at  35256  paddasslem12  35505  paddasslem13  35506  atmod1i1m  35532  lhp2lt  35675  lhpexle2lem  35683  lhpmcvr3  35699  lhpat3  35720  ltrneq2  35822  trlnle  35861  trlval3  35862  trlval4  35863  cdleme0moN  35900  cdleme17b  35962  cdlemefrs29pre00  36070  cdlemefr27cl  36078  cdleme42ke  36160  cdleme42mgN  36163  cdleme46f2g2  36168  cdleme46f2g1  36169  cdleme50eq  36216  cdleme50trn3  36228  trlord  36244  cdlemg6c  36295  cdlemg11b  36317  cdlemg18a  36353  cdlemg42  36404  cdlemg46  36410  trljco  36415  tendococl  36447  cdlemj3  36498  tendotr  36505  cdlemk35s-id  36613  cdlemk39s-id  36615  cdlemk53b  36631  cdlemk53  36632  cdlemk35u  36639  tendoex  36650  cdlemm10N  36794  dihopelvalcpre  36924  dihord6apre  36932  dihord5b  36935  dihglblem5apreN  36967  dihglblem2N  36970  dihmeetlem4preN  36982  dihmeetlem6  36985  dihmeetlem10N  36992  dihmeetlem11N  36993  dihmeetlem16N  36998  dihmeetlem17N  36999  dihmeetlem18N  37000  dihmeetlem19N  37001  dihmeetALTN  37003  dihlspsnat  37009  dvh3dim2  37124  dvh3dim3N  37125  jm2.25lem1  37952  jm2.26  37956  limcperiod  40248  0ellimcdiv  40269  cncfshift  40475  cncfperiod  40480  icccncfext  40488  stoweidlem34  40639  fourierdlem48  40759  fourierdlem87  40798  sge0xaddlem2  41039  smflimsuplem7  41423  domnmsuppn0  42545
  Copyright terms: Public domain W3C validator