Theorem simpl3r 1230

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  tfisi  7848  offsplitfpar  8105  omopth2  8584  ltmul1a  12063  xmulasslem3  13265  xadddi2  13276  swrdsbslen  14614  swrdspsleq  14615  dvdsadd2b  16249  pockthg  16839  psgnunilem4  19365  efgred  19616  marrepeval  22065  submaeval  22084  mdetmul  22125  minmar1eval  22151  ptbasin  23081  basqtop  23215  xrsmopn  24328  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  precsexlem8  27660  axpasch  28199  axeuclid  28221  elwwlks2ons3im  29208  br4  34728  btwnouttr2  34994  trisegint  35000  cgrxfr  35027  lineext  35048  btwnconn1lem13  35071  btwnconn1lem14  35072  btwnconn3  35075  brsegle  35080  brsegle2  35081  segleantisym  35087  outsideofeu  35103  lineunray  35119  lineelsb2  35120  cvrcmp  38153  atcvrj2b  38303  3dimlem3  38332  3dimlem3OLDN  38333  3dim3  38340  ps-1  38348  ps-2  38349  lplnnle2at  38412  2llnm3N  38440  4atlem0a  38464  4atlem3  38467  4atlem3a  38468  lnatexN  38650  paddasslem8  38698  paddasslem9  38699  paddasslem10  38700  paddasslem12  38702  paddasslem13  38703  lhpexle2lem  38880  lhpexle3  38883  lhpat3  38917  4atex  38947  trlval2  39034  trlval4  39059  cdleme16  39156  cdleme21  39208  cdleme21k  39209  cdleme27cl  39237  cdleme27N  39240  cdleme43fsv1snlem  39291  cdleme48fvg  39371  cdlemg8  39502  cdlemg15a  39526  cdlemg16z  39530  cdlemg24  39559  cdlemg38  39586  cdlemg40  39588  trlcone  39599  cdlemj2  39693  tendoid0  39696  tendoconid  39700  cdlemk34  39781  cdlemk38  39786  cdlemkid4  39805  cdlemk53  39828  tendospcanN  39894  dihvalcqpre  40106  dihmeetlem15N  40192  qirropth  41646  mzpcong  41711  jm2.26  41741  aomclem6  41801  islptre  44335  limccog  44336  limcleqr  44360  fourierdlem42  44865  elaa2  44950  itsclc0b  47458