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

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

Proof of Theorem simpl2l
StepHypRef Expression
1 simp2l 1080 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
21adantr 480 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  soisores  6477  omopth2  7551  fin23lem11  9022  dedekind  10079  xaddass  11951  swrdsbslen  13300  ntrivcvgmul  14473  pockthg  15448  gsmsymgreqlem2  17674  efgred  17984  decpmatmullem  20395  decpmatmul  20396  uncon  21042  basqtop  21324  utop2nei  21864  ucncn  21899  cxple2  24243  cxple2a  24245  ax5seglem1  25608  ax5seglem2  25609  axpasch  25621  axcontlem4  25647  wlklniswwlkn1  26227  cvmlift2lem10  30548  br4  30901  cgrcomim  31266  btwnintr  31296  btwnouttr2  31299  btwndiff  31304  btwnconn1lem14  31377  btwnconn3  31380  segcon2  31382  brsegle  31385  brsegle2  31386  segleantisym  31392  seglelin  31393  outsideofeu  31408  eqlkr  33404  eqlkr2  33405  lkrlsp  33407  atbtwn  33750  athgt  33760  3dimlem3  33765  3dimlem3OLDN  33766  3dim3  33773  3atlem7  33793  4atlem0a  33897  4atlem3a  33901  4atlem11  33913  lneq2at  34082  lnatexN  34083  cdlemb  34098  paddasslem6  34129  llnexchb2  34173  lhp2lt  34305  lhpexle2lem  34313  lhpexle3  34316  lhpmcvr3  34329  lhpat3  34350  ltrnnidn  34479  ltrneq3  34513  cdleme17b  34592  cdleme25a  34659  cdleme25dN  34662  cdleme27cl  34672  cdlemefrs29bpre0  34702  cdlemefs32sn1aw  34720  cdleme32le  34753  cdleme46f2g2  34799  cdleme46f2g1  34800  cdleme50trn3  34859  trlord  34875  ltrniotavalbN  34890  cdlemg6  34929  cdlemg7N  34932  cdlemg11b  34948  cdlemg15a  34961  cdlemg15  34962  cdlemg39  35022  trlcone  35034  cdlemg42  35035  tendoconid  35135  tendotr  35136  cdlemk39u  35274  cdlemk19u  35276  cdleml5N  35286  cdlemm10N  35425  dihord11b  35529  dihord2pre  35532  dihvalcqpre  35542  dihopelvalcpre  35555  dihord6apre  35563  dihord4  35565  dihord5b  35566  dihglblem5apreN  35598  dihmeetlem13N  35626  dihmeetlem19N  35632  dih1dimatlem0  35635  qirropth  36491  mzpcong  36557  jm2.25lem1  36583  jm2.26  36587  idomsubgmo  36795  fourierdlem42  39042  fourierdlem97  39096  1pthon2v-av  41320
  Copyright terms: Public domain W3C validator