Theorem simpl2r 1229

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simpl2r

Step	Hyp	Ref	Expression
1		simplr 769	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl2 1188	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  soisores  7275  omopth2  8512  ttrcltr  9628  fin23lem11  10230  xmulasslem3  13229  ssfzo12bi  13707  ntrivcvgmul  15858  pockthg  16868  gsumsgrpccat  18799  efgred  19714  lspfixed  21118  decpmatmullem  22746  decpmatmul  22747  unconn  23404  llyrest  23460  basqtop  23686  tmdgsum  24070  tsmsxp  24130  ucncn  24259  mulcxp  26662  cxple2  26674  nogt01o  27674  noetalem1  27719  cofcut1  27926  bdayfinbndlem1  28473  ax5seglem1  29011  ax5seglem2  29012  axpasch  29024  axcontlem4  29050  1pthon2v  30238  mhmimasplusg  33113  cvmlift2lem10  35510  br4  35956  cgrcomim  36187  btwnintr  36217  btwnouttr2  36220  btwndiff  36225  btwnconn1lem14  36298  btwnconn3  36301  segcon2  36303  brsegle  36306  brsegle2  36307  segleantisym  36313  outsideofeu  36329  eqlkr  39559  eqlkr2  39560  lkrlsp  39562  atbtwn  39906  3dimlem3OLDN  39922  3dim3  39929  3atlem7  39949  4atlem0a  40053  4atlem3a  40057  4atlem11  40069  lneq2at  40238  lnatexN  40239  paddasslem6  40285  llnexchb2  40329  lhpexle2lem  40469  lhpexle3  40472  lhp2at0nle  40495  lhpat3  40506  trlnid  40639  ltrneq3  40668  cdleme17b  40747  cdleme27cl  40826  cdlemefrs29bpre0  40856  cdlemefrs29clN  40859  cdlemefrs32fva  40860  cdlemefs32sn1aw  40874  cdleme32le  40907  ltrniotavalbN  41044  cdlemg6  41083  cdlemg7N  41086  cdlemg11b  41102  cdlemg15a  41115  cdlemg15  41116  cdlemg39  41176  trlcone  41188  cdlemg42  41189  tendoconid  41289  tendotr  41290  cdlemk39u  41428  cdlemk19u  41430  tendoex  41435  cdlemm10N  41578  dihord2pre  41685  dihord4  41718  dihord5b  41719  dihglbcpreN  41760  dihmeetlem13N  41779  dih1dimatlem0  41788  mzpcong  43418  jm2.25lem1  43444  jm2.26  43448  idomsubgmo  43639  uhgrimisgrgric  48419  itscnhlinecirc02plem2  49271