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 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:  tfisi  7801  offsplitfpar  8061  omopth2  8511  ltmul1a  11990  xmulasslem3  13201  xadddi2  13212  swrdsbslen  14588  swrdspsleq  14589  dvdsadd2b  16233  pockthg  16834  psgnunilem4  19426  efgred  19677  marrepeval  22507  submaeval  22526  mdetmul  22567  minmar1eval  22593  ptbasin  23521  basqtop  23655  xrsmopn  24757  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  precsexlem8  28210  axpasch  29014  axeuclid  29036  elwwlks2ons3im  30027  mhmimasplusg  33120  br4  35952  btwnouttr2  36216  trisegint  36222  cgrxfr  36249  lineext  36270  btwnconn1lem13  36293  btwnconn1lem14  36294  btwnconn3  36297  brsegle  36302  brsegle2  36303  segleantisym  36309  outsideofeu  36325  lineunray  36341  lineelsb2  36342  cvrcmp  39539  atcvrj2b  39688  3dimlem3  39717  3dimlem3OLDN  39718  3dim3  39725  ps-1  39733  ps-2  39734  lplnnle2at  39797  2llnm3N  39825  4atlem0a  39849  4atlem3  39852  4atlem3a  39853  lnatexN  40035  paddasslem8  40083  paddasslem9  40084  paddasslem10  40085  paddasslem12  40087  paddasslem13  40088  lhpexle2lem  40265  lhpexle3  40268  lhpat3  40302  4atex  40332  trlval2  40419  trlval4  40444  cdleme16  40541  cdleme21  40593  cdleme21k  40594  cdleme27cl  40622  cdleme27N  40625  cdleme43fsv1snlem  40676  cdleme48fvg  40756  cdlemg8  40887  cdlemg15a  40911  cdlemg16z  40915  cdlemg24  40944  cdlemg38  40971  cdlemg40  40973  trlcone  40984  cdlemj2  41078  tendoid0  41081  tendoconid  41085  cdlemk34  41166  cdlemk38  41171  cdlemkid4  41190  cdlemk53  41213  tendospcanN  41279  dihvalcqpre  41491  dihmeetlem15N  41577  qirropth  43146  mzpcong  43210  jm2.26  43240  aomclem6  43297  islptre  45861  limccog  45862  limcleqr  45884  fourierdlem42  46389  elaa2  46474  submodneaddmod  47593  itsclc0b  49014