Theorem simpl3r 1248

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl3r	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Proof of Theorem simpl3r

Step	Hyp	Ref	Expression
1		simplr 781	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl3 1206	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfisi  7870  offsplitfpar  8132  omopth2  8595  ltmul1a  12169  xmulasslem3  13419  xadddi2  13430  swrdsbslen  14818  swrdspsleq  14819  dvdsadd2b  16481  pockthg  17089  psgnunilem4  19716  efgred  19967  marrepeval  22883  submaeval  22902  mdetmul  22943  minmar1eval  22969  ptbasin  23901  basqtop  24035  xrsmopn  25137  nosupbnd1lem3  28072  nosupbnd1lem4  28073  nosupbnd1lem5  28074  noinfbnd1lem3  28087  noinfbnd1lem4  28088  noinfbnd1lem5  28089  precsexlem8  28605  axpasch  29524  axeuclid  29546  elwwlks2ons3im  30548  mhmimasplusg  33644  br4  36615  btwnouttr2  36879  trisegint  36885  cgrxfr  36912  lineext  36933  btwnconn1lem13  36956  btwnconn1lem14  36957  btwnconn3  36960  brsegle  36965  brsegle2  36966  segleantisym  36972  outsideofeu  36988  lineunray  37004  lineelsb2  37005  cvrcmp  40433  atcvrj2b  40582  3dimlem3  40611  3dimlem3OLDN  40612  3dim3  40619  ps-1  40627  ps-2  40628  lplnnle2at  40691  2llnm3N  40719  4atlem0a  40743  4atlem3  40746  4atlem3a  40747  lnatexN  40929  paddasslem8  40977  paddasslem9  40978  paddasslem10  40979  paddasslem12  40981  paddasslem13  40982  lhpexle2lem  41159  lhpexle3  41162  lhpat3  41196  4atex  41226  trlval2  41313  trlval4  41338  cdleme16  41435  cdleme21  41487  cdleme21k  41488  cdleme27cl  41516  cdleme27N  41519  cdleme43fsv1snlem  41570  cdleme48fvg  41650  cdlemg8  41781  cdlemg15a  41805  cdlemg16z  41809  cdlemg24  41838  cdlemg38  41865  cdlemg40  41867  trlcone  41878  cdlemj2  41972  tendoid0  41975  tendoconid  41979  cdlemk34  42060  cdlemk38  42065  cdlemkid4  42084  cdlemk53  42107  tendospcanN  42173  dihvalcqpre  42385  dihmeetlem15N  42471  qirropth  44008  mzpcong  44072  jm2.26  44102  aomclem6  44154  islptre  46724  limccog  46725  limcleqr  46747  fourierdlem42  47252  elaa2  47337  submodneaddmod  48520  itsclc0b  49977