Theorem simpl3r 1225

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  tfisi  7575  offsplitfpar  7817  omopth2  8212  ltmul1a  11491  xmulasslem3  12682  xadddi2  12693  swrdsbslen  14028  swrdspsleq  14029  dvdsadd2b  15658  pockthg  16244  psgnunilem4  18627  efgred  18876  marrepeval  21174  submaeval  21193  mdetmul  21234  minmar1eval  21260  ptbasin  22187  basqtop  22321  xrsmopn  23422  axpasch  26729  axeuclid  26751  elwwlks2ons3im  27735  br4  32996  nosupbnd1lem3  33212  nosupbnd1lem4  33213  nosupbnd1lem5  33214  btwnouttr2  33485  trisegint  33491  cgrxfr  33518  lineext  33539  btwnconn1lem13  33562  btwnconn1lem14  33563  btwnconn3  33566  brsegle  33571  brsegle2  33572  segleantisym  33578  outsideofeu  33594  lineunray  33610  lineelsb2  33611  cvrcmp  36421  atcvrj2b  36570  3dimlem3  36599  3dimlem3OLDN  36600  3dim3  36607  ps-1  36615  ps-2  36616  lplnnle2at  36679  2llnm3N  36707  4atlem0a  36731  4atlem3  36734  4atlem3a  36735  lnatexN  36917  paddasslem8  36965  paddasslem9  36966  paddasslem10  36967  paddasslem12  36969  paddasslem13  36970  lhpexle2lem  37147  lhpexle3  37150  lhpat3  37184  4atex  37214  trlval2  37301  trlval4  37326  cdleme16  37423  cdleme21  37475  cdleme21k  37476  cdleme27cl  37504  cdleme27N  37507  cdleme43fsv1snlem  37558  cdleme48fvg  37638  cdlemg8  37769  cdlemg15a  37793  cdlemg16z  37797  cdlemg24  37826  cdlemg38  37853  cdlemg40  37855  trlcone  37866  cdlemj2  37960  tendoid0  37963  tendoconid  37967  cdlemk34  38048  cdlemk38  38053  cdlemkid4  38072  cdlemk53  38095  tendospcanN  38161  dihvalcqpre  38373  dihmeetlem15N  38459  qirropth  39512  mzpcong  39576  jm2.26  39606  aomclem6  39666  islptre  41907  limccog  41908  limcleqr  41932  fourierdlem42  42441  elaa2  42526  itsclc0b  44766