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  7801  omopth2  8510  ltmul1a  11993  xaddass  13190  xlemul2a  13230  swrdsbslen  14616  swrdspsleq  14617  dvdsadd2b  16264  pockthg  16866  psgnunilem4  19461  efgred  19712  ptbasin  23551  basqtop  23685  xrsmopn  24787  nosupbnd1lem3  27693  nosupbnd1lem4  27694  noinfbnd1lem3  27708  noinfbnd1lem4  27709  noinfbnd1lem5  27710  precsexlem8  28225  bdayfinbndlem1  28478  axpasch  29029  axcontlem4  29055  elwwlks2ons3im  30042  mhmimasplusg  33118  br4  35961  btwnintr  36222  btwnexch3  36223  btwnouttr2  36225  cgrxfr  36258  lineext  36279  btwnconn1lem13  36302  btwnconn1lem14  36303  btwnconn3  36306  brsegle  36311  brsegle2  36312  segleantisym  36318  outsideofeu  36334  lineunray  36350  lineelsb2  36351  cvrcmp  39740  atcvrj2b  39889  3dimlem3  39918  3dimlem3OLDN  39919  3dim3  39926  ps-1  39934  lplnnle2at  39998  2llnm3N  40026  lvolnle3at  40039  4atlem0a  40050  4atlem3  40053  4atlem3a  40054  lnatexN  40236  paddasslem8  40284  paddasslem9  40285  paddasslem10  40286  paddasslem12  40288  paddasslem13  40289  lhp2lt  40458  lhpexle2lem  40466  lhpexle3  40469  lhpmcvr3  40482  lhpat3  40503  4atex  40533  trlval2  40620  ltrnideq  40632  ltrnatlw  40640  trlnle  40643  trlval4  40645  cdlemd4  40658  cdlemd5  40659  cdleme16  40742  cdleme21  40794  cdleme21k  40795  cdleme27cl  40823  cdleme27N  40826  cdleme29ex  40831  cdleme43fsv1snlem  40877  cdleme40m  40924  cdleme46f2g2  40950  cdleme46f2g1  40951  trlord  41026  cdlemg8  41088  cdlemg15a  41112  cdlemg16z  41116  cdlemg18a  41135  cdlemg24  41145  cdlemg38  41172  cdlemg40  41174  trlcone  41185  cdlemj2  41279  tendoid0  41282  tendoconid  41286  cdlemk34  41367  cdlemk38  41372  cdlemkid4  41391  cdlemk35s-id  41395  cdlemk39s-id  41397  cdlemk53  41414  tendospcanN  41480  cdlemm10N  41575  dihvalcqpre  41692  dihopelvalcpre  41705  dihord5b  41716  dihglblem5apreN  41748  dihmeetlem16N  41779  dihmeetlem17N  41780  dvh3dim3N  41906  qirropth  43351  mzpcong  43415  jm2.26  43445  aomclem6  43502  limcleqr  46087  fourierdlem42  46592  submodneaddmod  47802  itsclc0b  49245