Theorem simpl3r 1229

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 1187	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  tfisi  7800  offsplitfpar  8056  omopth2  8536  ltmul1a  12013  xmulasslem3  13215  xadddi2  13226  swrdsbslen  14564  swrdspsleq  14565  dvdsadd2b  16199  pockthg  16789  psgnunilem4  19293  efgred  19544  marrepeval  21949  submaeval  21968  mdetmul  22009  minmar1eval  22035  ptbasin  22965  basqtop  23099  xrsmopn  24212  nosupbnd1lem3  27095  nosupbnd1lem4  27096  nosupbnd1lem5  27097  noinfbnd1lem3  27110  noinfbnd1lem4  27111  noinfbnd1lem5  27112  axpasch  27953  axeuclid  27975  elwwlks2ons3im  28962  br4  34417  btwnouttr2  34683  trisegint  34689  cgrxfr  34716  lineext  34737  btwnconn1lem13  34760  btwnconn1lem14  34761  btwnconn3  34764  brsegle  34769  brsegle2  34770  segleantisym  34776  outsideofeu  34792  lineunray  34808  lineelsb2  34809  cvrcmp  37818  atcvrj2b  37968  3dimlem3  37997  3dimlem3OLDN  37998  3dim3  38005  ps-1  38013  ps-2  38014  lplnnle2at  38077  2llnm3N  38105  4atlem0a  38129  4atlem3  38132  4atlem3a  38133  lnatexN  38315  paddasslem8  38363  paddasslem9  38364  paddasslem10  38365  paddasslem12  38367  paddasslem13  38368  lhpexle2lem  38545  lhpexle3  38548  lhpat3  38582  4atex  38612  trlval2  38699  trlval4  38724  cdleme16  38821  cdleme21  38873  cdleme21k  38874  cdleme27cl  38902  cdleme27N  38905  cdleme43fsv1snlem  38956  cdleme48fvg  39036  cdlemg8  39167  cdlemg15a  39191  cdlemg16z  39195  cdlemg24  39224  cdlemg38  39251  cdlemg40  39253  trlcone  39264  cdlemj2  39358  tendoid0  39361  tendoconid  39365  cdlemk34  39446  cdlemk38  39451  cdlemkid4  39470  cdlemk53  39493  tendospcanN  39559  dihvalcqpre  39771  dihmeetlem15N  39857  qirropth  41289  mzpcong  41354  jm2.26  41384  aomclem6  41444  islptre  43980  limccog  43981  limcleqr  44005  fourierdlem42  44510  elaa2  44595  itsclc0b  46978