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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soisores  7327  omopth2  8570  ttrcltr  9686  fin23lem11  10302  xmulasslem3  13313  ssfzo12bi  13792  ntrivcvgmul  15958  pockthg  16967  gsumsgrpccat  18900  efgred  19819  lspfixed  21233  decpmatmullem  22909  decpmatmul  22910  unconn  23567  llyrest  23623  basqtop  23849  tmdgsum  24233  tsmsxp  24293  ucncn  24422  mulcxp  26831  cxple2  26843  nogt01o  27841  noetalem1  27886  cofcut1  28094  bdayfinbndlem1  28641  ax5seglem1  29259  ax5seglem2  29260  axpasch  29272  axcontlem4  29298  1pthon2v  30485  mhmimasplusg  33338  cvmlift2lem10  35785  br4  36231  cgrcomim  36462  btwnintr  36492  btwnouttr2  36495  btwndiff  36500  btwnconn1lem14  36573  btwnconn3  36576  segcon2  36578  brsegle  36581  brsegle2  36582  segleantisym  36588  outsideofeu  36604  eqlkr  39854  eqlkr2  39855  lkrlsp  39857  atbtwn  40201  3dimlem3OLDN  40217  3dim3  40224  3atlem7  40244  4atlem0a  40348  4atlem3a  40352  4atlem11  40364  lneq2at  40533  lnatexN  40534  paddasslem6  40580  llnexchb2  40624  lhpexle2lem  40764  lhpexle3  40767  lhp2at0nle  40790  lhpat3  40801  trlnid  40934  ltrneq3  40963  cdleme17b  41042  cdleme27cl  41121  cdlemefrs29bpre0  41151  cdlemefrs29clN  41154  cdlemefrs32fva  41155  cdlemefs32sn1aw  41169  cdleme32le  41202  ltrniotavalbN  41339  cdlemg6  41378  cdlemg7N  41381  cdlemg11b  41397  cdlemg15a  41410  cdlemg15  41411  cdlemg39  41471  trlcone  41483  cdlemg42  41484  tendoconid  41584  tendotr  41585  cdlemk39u  41723  cdlemk19u  41725  tendoex  41730  cdlemm10N  41873  dihord2pre  41980  dihord4  42013  dihord5b  42014  dihglbcpreN  42055  dihmeetlem13N  42074  dih1dimatlem0  42083  mzpcong  43682  jm2.25lem1  43708  jm2.26  43712  idomsubgmo  43903  uhgrimisgrgric  48679  itscnhlinecirc02plem2  49546