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  7273  omopth2  8511  ttrcltr  9625  fin23lem11  10227  xmulasslem3  13201  ssfzo12bi  13677  ntrivcvgmul  15825  pockthg  16834  gsumsgrpccat  18765  efgred  19677  lspfixed  21083  decpmatmullem  22715  decpmatmul  22716  unconn  23373  llyrest  23429  basqtop  23655  tmdgsum  24039  tsmsxp  24099  ucncn  24228  mulcxp  26650  cxple2  26662  nogt01o  27664  noetalem1  27709  cofcut1  27916  bdayfinbndlem1  28463  ax5seglem1  29001  ax5seglem2  29002  axpasch  29014  axcontlem4  29040  1pthon2v  30228  mhmimasplusg  33120  cvmlift2lem10  35506  br4  35952  cgrcomim  36183  btwnintr  36213  btwnouttr2  36216  btwndiff  36221  btwnconn1lem14  36294  btwnconn3  36297  segcon2  36299  brsegle  36302  brsegle2  36303  segleantisym  36309  outsideofeu  36325  eqlkr  39355  eqlkr2  39356  lkrlsp  39358  atbtwn  39702  3dimlem3OLDN  39718  3dim3  39725  3atlem7  39745  4atlem0a  39849  4atlem3a  39853  4atlem11  39865  lneq2at  40034  lnatexN  40035  paddasslem6  40081  llnexchb2  40125  lhpexle2lem  40265  lhpexle3  40268  lhp2at0nle  40291  lhpat3  40302  trlnid  40435  ltrneq3  40464  cdleme17b  40543  cdleme27cl  40622  cdlemefrs29bpre0  40652  cdlemefrs29clN  40655  cdlemefrs32fva  40656  cdlemefs32sn1aw  40670  cdleme32le  40703  ltrniotavalbN  40840  cdlemg6  40879  cdlemg7N  40882  cdlemg11b  40898  cdlemg15a  40911  cdlemg15  40912  cdlemg39  40972  trlcone  40984  cdlemg42  40985  tendoconid  41085  tendotr  41086  cdlemk39u  41224  cdlemk19u  41226  tendoex  41231  cdlemm10N  41374  dihord2pre  41481  dihord4  41514  dihord5b  41515  dihglbcpreN  41556  dihmeetlem13N  41575  dih1dimatlem0  41584  mzpcong  43210  jm2.25lem1  43236  jm2.26  43240  idomsubgmo  43431  uhgrimisgrgric  48173  itscnhlinecirc02plem2  49025