Theorem simpl2r 1108

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

Assertion

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

Proof of Theorem simpl2r

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

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  xmulasslem3  11988  ssfzo12bi  12429  ntrivcvgmul  14473  pockthg  15448  gsmsymgreqlem2  17674  efgred  17984  lspfixed  18949  decpmatmullem  20395  decpmatmul  20396  uncon  21042  llyrest  21098  basqtop  21324  tmdgsum  21709  tsmsxp  21768  ucncn  21899  mulcxp  24231  cxple2  24243  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  outsideofeu  31408  eqlkr  33404  eqlkr2  33405  lkrlsp  33407  atbtwn  33750  3dimlem3OLDN  33766  3dim3  33773  3atlem7  33793  4atlem0a  33897  4atlem3a  33901  4atlem11  33913  lneq2at  34082  lnatexN  34083  paddasslem6  34129  llnexchb2  34173  lhpexle2lem  34313  lhpexle3  34316  lhp2at0nle  34339  lhpat3  34350  trlnid  34484  ltrneq3  34513  cdleme17b  34592  cdleme27cl  34672  cdlemefrs29bpre0  34702  cdlemefrs29clN  34705  cdlemefrs32fva  34706  cdlemefs32sn1aw  34720  cdleme32le  34753  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  tendoex  35281  cdlemm10N  35425  dihord2pre  35532  dihord4  35565  dihord5b  35566  dihglbcpreN  35607  dihmeetlem13N  35626  dih1dimatlem0  35635  mzpcong  36557  jm2.25lem1  36583  jm2.26  36587  idomsubgmo  36795  1pthon2v-av  41320