Theorem simpl2r 1227

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  soisores  7326  omopth2  8586  ttrcltr  9713  fin23lem11  10314  xmulasslem3  13269  ssfzo12bi  13731  ntrivcvgmul  15852  pockthg  16843  gsumsgrpccat  18757  efgred  19657  lspfixed  20886  decpmatmullem  22493  decpmatmul  22494  unconn  23153  llyrest  23209  basqtop  23435  tmdgsum  23819  tsmsxp  23879  ucncn  24010  mulcxp  26417  cxple2  26429  nogt01o  27423  noetalem1  27468  cofcut1  27633  ax5seglem1  28441  ax5seglem2  28442  axpasch  28454  axcontlem4  28480  1pthon2v  29661  mhmimasplusg  32454  cvmlift2lem10  34589  br4  35020  cgrcomim  35253  btwnintr  35283  btwnouttr2  35286  btwndiff  35291  btwnconn1lem14  35364  btwnconn3  35367  segcon2  35369  brsegle  35372  brsegle2  35373  segleantisym  35379  outsideofeu  35395  eqlkr  38272  eqlkr2  38273  lkrlsp  38275  atbtwn  38620  3dimlem3OLDN  38636  3dim3  38643  3atlem7  38663  4atlem0a  38767  4atlem3a  38771  4atlem11  38783  lneq2at  38952  lnatexN  38953  paddasslem6  38999  llnexchb2  39043  lhpexle2lem  39183  lhpexle3  39186  lhp2at0nle  39209  lhpat3  39220  trlnid  39353  ltrneq3  39382  cdleme17b  39461  cdleme27cl  39540  cdlemefrs29bpre0  39570  cdlemefrs29clN  39573  cdlemefrs32fva  39574  cdlemefs32sn1aw  39588  cdleme32le  39621  ltrniotavalbN  39758  cdlemg6  39797  cdlemg7N  39800  cdlemg11b  39816  cdlemg15a  39829  cdlemg15  39830  cdlemg39  39890  trlcone  39902  cdlemg42  39903  tendoconid  40003  tendotr  40004  cdlemk39u  40142  cdlemk19u  40144  tendoex  40149  cdlemm10N  40292  dihord2pre  40399  dihord4  40432  dihord5b  40433  dihglbcpreN  40474  dihmeetlem13N  40493  dih1dimatlem0  40502  mzpcong  42013  jm2.25lem1  42039  jm2.26  42043  idomsubgmo  42242  itscnhlinecirc02plem2  47557