Theorem simpl3l 1230

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

Assertion

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

Proof of Theorem simpl3l

Step	Hyp	Ref	Expression
1		simpll 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1189	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  tfisi  7810  omopth2  8519  ltmul1a  12004  xaddass  13201  xlemul2a  13241  swrdsbslen  14627  swrdspsleq  14628  dvdsadd2b  16275  pockthg  16877  psgnunilem4  19472  efgred  19723  ptbasin  23542  basqtop  23676  xrsmopn  24778  nosupbnd1lem3  27674  nosupbnd1lem4  27675  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  precsexlem8  28206  bdayfinbndlem1  28459  axpasch  29010  axcontlem4  29036  elwwlks2ons3im  30022  mhmimasplusg  33098  br4  35940  btwnintr  36201  btwnexch3  36202  btwnouttr2  36204  cgrxfr  36237  lineext  36258  btwnconn1lem13  36281  btwnconn1lem14  36282  btwnconn3  36285  brsegle  36290  brsegle2  36291  segleantisym  36297  outsideofeu  36313  lineunray  36329  lineelsb2  36330  cvrcmp  39729  atcvrj2b  39878  3dimlem3  39907  3dimlem3OLDN  39908  3dim3  39915  ps-1  39923  lplnnle2at  39987  2llnm3N  40015  lvolnle3at  40028  4atlem0a  40039  4atlem3  40042  4atlem3a  40043  lnatexN  40225  paddasslem8  40273  paddasslem9  40274  paddasslem10  40275  paddasslem12  40277  paddasslem13  40278  lhp2lt  40447  lhpexle2lem  40455  lhpexle3  40458  lhpmcvr3  40471  lhpat3  40492  4atex  40522  trlval2  40609  ltrnideq  40621  ltrnatlw  40629  trlnle  40632  trlval4  40634  cdlemd4  40647  cdlemd5  40648  cdleme16  40731  cdleme21  40783  cdleme21k  40784  cdleme27cl  40812  cdleme27N  40815  cdleme29ex  40820  cdleme43fsv1snlem  40866  cdleme40m  40913  cdleme46f2g2  40939  cdleme46f2g1  40940  trlord  41015  cdlemg8  41077  cdlemg15a  41101  cdlemg16z  41105  cdlemg18a  41124  cdlemg24  41134  cdlemg38  41161  cdlemg40  41163  trlcone  41174  cdlemj2  41268  tendoid0  41271  tendoconid  41275  cdlemk34  41356  cdlemk38  41361  cdlemkid4  41380  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk53  41403  tendospcanN  41469  cdlemm10N  41564  dihvalcqpre  41681  dihopelvalcpre  41694  dihord5b  41705  dihglblem5apreN  41737  dihmeetlem16N  41768  dihmeetlem17N  41769  dvh3dim3N  41895  qirropth  43336  mzpcong  43400  jm2.26  43430  aomclem6  43487  limcleqr  46072  fourierdlem42  46577  submodneaddmod  47799  itsclc0b  49242