Theorem simpl2r 1246

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 781	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl2 1205	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7335  omopth2  8595  ttrcltr  9720  fin23lem11  10398  xmulasslem3  13419  ssfzo12bi  13899  ntrivcvgmul  16076  pockthg  17089  gsumsgrpccat  19041  efgred  19967  lspfixed  21411  decpmatmullem  23094  decpmatmul  23095  unconn  23752  llyrest  23809  basqtop  24035  tmdgsum  24419  tsmsxp  24479  ucncn  24608  mulcxp  27018  cxple2  27030  nogt01o  28058  noetalem1  28103  cofcut1  28311  bdayfinbndlem1  28858  ax5seglem1  29511  ax5seglem2  29512  axpasch  29524  axcontlem4  29550  1pthon2v  30759  mhmimasplusg  33644  cvmlift2lem10  36163  br4  36615  cgrcomim  36846  btwnintr  36876  btwnouttr2  36879  btwndiff  36884  btwnconn1lem14  36957  btwnconn3  36960  segcon2  36962  brsegle  36965  brsegle2  36966  segleantisym  36972  outsideofeu  36988  eqlkr  40249  eqlkr2  40250  lkrlsp  40252  atbtwn  40596  3dimlem3OLDN  40612  3dim3  40619  3atlem7  40639  4atlem0a  40743  4atlem3a  40747  4atlem11  40759  lneq2at  40928  lnatexN  40929  paddasslem6  40975  llnexchb2  41019  lhpexle2lem  41159  lhpexle3  41162  lhp2at0nle  41185  lhpat3  41196  trlnid  41329  ltrneq3  41358  cdleme17b  41437  cdleme27cl  41516  cdlemefrs29bpre0  41546  cdlemefrs29clN  41549  cdlemefrs32fva  41550  cdlemefs32sn1aw  41564  cdleme32le  41597  ltrniotavalbN  41734  cdlemg6  41773  cdlemg7N  41776  cdlemg11b  41792  cdlemg15a  41805  cdlemg15  41806  cdlemg39  41866  trlcone  41878  cdlemg42  41879  tendoconid  41979  tendotr  41980  cdlemk39u  42118  cdlemk19u  42120  tendoex  42125  cdlemm10N  42268  dihord2pre  42375  dihord4  42408  dihord5b  42409  dihglbcpreN  42450  dihmeetlem13N  42469  dih1dimatlem0  42478  mzpcong  44072  jm2.25lem1  44098  jm2.26  44102  idomsubgmo  44288  uhgrimisgrgric  49122  itscnhlinecirc02plem2  49988