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

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

Proof of Theorem simpl2r
StepHypRef Expression
1 simp2r 1086 . 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  9091  xmulasslem3  12067  ssfzo12bi  12512  ntrivcvgmul  14570  pockthg  15545  gsmsymgreqlem2  17783  efgred  18093  lspfixed  19060  decpmatmullem  20508  decpmatmul  20509  unconn  21155  llyrest  21211  basqtop  21437  tmdgsum  21822  tsmsxp  21881  ucncn  22012  mulcxp  24348  cxple2  24360  ax5seglem1  25725  ax5seglem2  25726  axpasch  25738  axcontlem4  25764  1pthon2v  26896  cvmlift2lem10  31037  br4  31391  noprefixmo  31608  cgrcomim  31773  btwnintr  31803  btwnouttr2  31806  btwndiff  31811  btwnconn1lem14  31884  btwnconn3  31887  segcon2  31889  brsegle  31892  brsegle2  31893  segleantisym  31899  outsideofeu  31915  eqlkr  33901  eqlkr2  33902  lkrlsp  33904  atbtwn  34247  3dimlem3OLDN  34263  3dim3  34270  3atlem7  34290  4atlem0a  34394  4atlem3a  34398  4atlem11  34410  lneq2at  34579  lnatexN  34580  paddasslem6  34626  llnexchb2  34670  lhpexle2lem  34810  lhpexle3  34813  lhp2at0nle  34836  lhpat3  34847  trlnid  34981  ltrneq3  35010  cdleme17b  35089  cdleme27cl  35169  cdlemefrs29bpre0  35199  cdlemefrs29clN  35202  cdlemefrs32fva  35203  cdlemefs32sn1aw  35217  cdleme32le  35250  ltrniotavalbN  35387  cdlemg6  35426  cdlemg7N  35429  cdlemg11b  35445  cdlemg15a  35458  cdlemg15  35459  cdlemg39  35519  trlcone  35531  cdlemg42  35532  tendoconid  35632  tendotr  35633  cdlemk39u  35771  cdlemk19u  35773  tendoex  35778  cdlemm10N  35922  dihord2pre  36029  dihord4  36062  dihord5b  36063  dihglbcpreN  36104  dihmeetlem13N  36123  dih1dimatlem0  36132  mzpcong  37054  jm2.25lem1  37080  jm2.26  37084  idomsubgmo  37292
  Copyright terms: Public domain W3C validator