Theorem simpl2r 1115

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl2r	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpl2r

Step	Hyp	Ref	Expression
1		simp2r 1088	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	adantr 481	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 1039

This theorem is referenced by:  soisores  6577  omopth2  7664  fin23lem11  9139  xmulasslem3  12116  ssfzo12bi  12563  ntrivcvgmul  14634  pockthg  15610  gsmsymgreqlem2  17851  efgred  18161  lspfixed  19128  decpmatmullem  20576  decpmatmul  20577  unconn  21232  llyrest  21288  basqtop  21514  tmdgsum  21899  tsmsxp  21958  ucncn  22089  mulcxp  24431  cxple2  24443  ax5seglem1  25808  ax5seglem2  25809  axpasch  25821  axcontlem4  25847  1pthon2v  27013  cvmlift2lem10  31294  br4  31648  cgrcomim  32096  btwnintr  32126  btwnouttr2  32129  btwndiff  32134  btwnconn1lem14  32207  btwnconn3  32210  segcon2  32212  brsegle  32215  brsegle2  32216  segleantisym  32222  outsideofeu  32238  eqlkr  34386  eqlkr2  34387  lkrlsp  34389  atbtwn  34732  3dimlem3OLDN  34748  3dim3  34755  3atlem7  34775  4atlem0a  34879  4atlem3a  34883  4atlem11  34895  lneq2at  35064  lnatexN  35065  paddasslem6  35111  llnexchb2  35155  lhpexle2lem  35295  lhpexle3  35298  lhp2at0nle  35321  lhpat3  35332  trlnid  35466  ltrneq3  35495  cdleme17b  35574  cdleme27cl  35654  cdlemefrs29bpre0  35684  cdlemefrs29clN  35687  cdlemefrs32fva  35688  cdlemefs32sn1aw  35702  cdleme32le  35735  ltrniotavalbN  35872  cdlemg6  35911  cdlemg7N  35914  cdlemg11b  35930  cdlemg15a  35943  cdlemg15  35944  cdlemg39  36004  trlcone  36016  cdlemg42  36017  tendoconid  36117  tendotr  36118  cdlemk39u  36256  cdlemk19u  36258  tendoex  36263  cdlemm10N  36407  dihord2pre  36514  dihord4  36547  dihord5b  36548  dihglbcpreN  36589  dihmeetlem13N  36608  dih1dimatlem0  36617  mzpcong  37539  jm2.25lem1  37565  jm2.26  37569  idomsubgmo  37776