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  7325  omopth2  8601  ttrcltr  9735  fin23lem11  10336  xmulasslem3  13307  ssfzo12bi  13782  ntrivcvgmul  15923  pockthg  16931  gsumsgrpccat  18823  efgred  19734  lspfixed  21094  decpmatmullem  22714  decpmatmul  22715  unconn  23372  llyrest  23428  basqtop  23654  tmdgsum  24038  tsmsxp  24098  ucncn  24228  mulcxp  26651  cxple2  26663  nogt01o  27665  noetalem1  27710  cofcut1  27885  ax5seglem1  28912  ax5seglem2  28913  axpasch  28925  axcontlem4  28951  1pthon2v  30139  mhmimasplusg  33038  cvmlift2lem10  35339  br4  35780  cgrcomim  36012  btwnintr  36042  btwnouttr2  36045  btwndiff  36050  btwnconn1lem14  36123  btwnconn3  36126  segcon2  36128  brsegle  36131  brsegle2  36132  segleantisym  36138  outsideofeu  36154  eqlkr  39122  eqlkr2  39123  lkrlsp  39125  atbtwn  39470  3dimlem3OLDN  39486  3dim3  39493  3atlem7  39513  4atlem0a  39617  4atlem3a  39621  4atlem11  39633  lneq2at  39802  lnatexN  39803  paddasslem6  39849  llnexchb2  39893  lhpexle2lem  40033  lhpexle3  40036  lhp2at0nle  40059  lhpat3  40070  trlnid  40203  ltrneq3  40232  cdleme17b  40311  cdleme27cl  40390  cdlemefrs29bpre0  40420  cdlemefrs29clN  40423  cdlemefrs32fva  40424  cdlemefs32sn1aw  40438  cdleme32le  40471  ltrniotavalbN  40608  cdlemg6  40647  cdlemg7N  40650  cdlemg11b  40666  cdlemg15a  40679  cdlemg15  40680  cdlemg39  40740  trlcone  40752  cdlemg42  40753  tendoconid  40853  tendotr  40854  cdlemk39u  40992  cdlemk19u  40994  tendoex  40999  cdlemm10N  41142  dihord2pre  41249  dihord4  41282  dihord5b  41283  dihglbcpreN  41324  dihmeetlem13N  41343  dih1dimatlem0  41352  mzpcong  42963  jm2.25lem1  42989  jm2.26  42993  idomsubgmo  43184  uhgrimisgrgric  47911  itscnhlinecirc02plem2  48730