Theorem simpl2r 1240

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  soisores  7307  omopth2  8548  ttrcltr  9668  fin23lem11  10271  xmulasslem3  13286  ssfzo12bi  13764  ntrivcvgmul  15915  pockthg  16925  gsumsgrpccat  18857  efgred  19771  lspfixed  21178  decpmatmullem  22811  decpmatmul  22812  unconn  23469  llyrest  23525  basqtop  23751  tmdgsum  24135  tsmsxp  24195  ucncn  24324  mulcxp  26727  cxple2  26739  nogt01o  27737  noetalem1  27782  cofcut1  27990  bdayfinbndlem1  28537  ax5seglem1  29075  ax5seglem2  29076  axpasch  29088  axcontlem4  29114  1pthon2v  30301  mhmimasplusg  33177  cvmlift2lem10  35626  br4  36072  cgrcomim  36303  btwnintr  36333  btwnouttr2  36336  btwndiff  36341  btwnconn1lem14  36414  btwnconn3  36417  segcon2  36419  brsegle  36422  brsegle2  36423  segleantisym  36429  outsideofeu  36445  eqlkr  39687  eqlkr2  39688  lkrlsp  39690  atbtwn  40034  3dimlem3OLDN  40050  3dim3  40057  3atlem7  40077  4atlem0a  40181  4atlem3a  40185  4atlem11  40197  lneq2at  40366  lnatexN  40367  paddasslem6  40413  llnexchb2  40457  lhpexle2lem  40597  lhpexle3  40600  lhp2at0nle  40623  lhpat3  40634  trlnid  40767  ltrneq3  40796  cdleme17b  40875  cdleme27cl  40954  cdlemefrs29bpre0  40984  cdlemefrs29clN  40987  cdlemefrs32fva  40988  cdlemefs32sn1aw  41002  cdleme32le  41035  ltrniotavalbN  41172  cdlemg6  41211  cdlemg7N  41214  cdlemg11b  41230  cdlemg15a  41243  cdlemg15  41244  cdlemg39  41304  trlcone  41316  cdlemg42  41317  tendoconid  41417  tendotr  41418  cdlemk39u  41556  cdlemk19u  41558  tendoex  41563  cdlemm10N  41706  dihord2pre  41813  dihord4  41846  dihord5b  41847  dihglbcpreN  41888  dihmeetlem13N  41907  dih1dimatlem0  41916  mzpcong  43513  jm2.25lem1  43539  jm2.26  43543  idomsubgmo  43734  uhgrimisgrgric  48517  itscnhlinecirc02plem2  49369