Theorem simpl2r 1228

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

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

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 1088

This theorem is referenced by:  soisores  7305  omopth2  8551  ttrcltr  9676  fin23lem11  10277  xmulasslem3  13253  ssfzo12bi  13729  ntrivcvgmul  15875  pockthg  16884  gsumsgrpccat  18774  efgred  19685  lspfixed  21045  decpmatmullem  22665  decpmatmul  22666  unconn  23323  llyrest  23379  basqtop  23605  tmdgsum  23989  tsmsxp  24049  ucncn  24179  mulcxp  26601  cxple2  26613  nogt01o  27615  noetalem1  27660  cofcut1  27835  ax5seglem1  28862  ax5seglem2  28863  axpasch  28875  axcontlem4  28901  1pthon2v  30089  mhmimasplusg  32986  cvmlift2lem10  35306  br4  35752  cgrcomim  35984  btwnintr  36014  btwnouttr2  36017  btwndiff  36022  btwnconn1lem14  36095  btwnconn3  36098  segcon2  36100  brsegle  36103  brsegle2  36104  segleantisym  36110  outsideofeu  36126  eqlkr  39099  eqlkr2  39100  lkrlsp  39102  atbtwn  39447  3dimlem3OLDN  39463  3dim3  39470  3atlem7  39490  4atlem0a  39594  4atlem3a  39598  4atlem11  39610  lneq2at  39779  lnatexN  39780  paddasslem6  39826  llnexchb2  39870  lhpexle2lem  40010  lhpexle3  40013  lhp2at0nle  40036  lhpat3  40047  trlnid  40180  ltrneq3  40209  cdleme17b  40288  cdleme27cl  40367  cdlemefrs29bpre0  40397  cdlemefrs29clN  40400  cdlemefrs32fva  40401  cdlemefs32sn1aw  40415  cdleme32le  40448  ltrniotavalbN  40585  cdlemg6  40624  cdlemg7N  40627  cdlemg11b  40643  cdlemg15a  40656  cdlemg15  40657  cdlemg39  40717  trlcone  40729  cdlemg42  40730  tendoconid  40830  tendotr  40831  cdlemk39u  40969  cdlemk19u  40971  tendoex  40976  cdlemm10N  41119  dihord2pre  41226  dihord4  41259  dihord5b  41260  dihglbcpreN  41301  dihmeetlem13N  41320  dih1dimatlem0  41329  mzpcong  42968  jm2.25lem1  42994  jm2.26  42998  idomsubgmo  43189  uhgrimisgrgric  47935  itscnhlinecirc02plem2  48776