Theorem simpl3l 1246

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  tfisi  7853  omopth2  8567  ltmul1a  12070  xaddass  13281  xlemul2a  13321  swrdsbslen  14709  swrdspsleq  14710  dvdsadd2b  16370  pockthg  16972  psgnunilem4  19573  efgred  19824  ptbasin  23745  basqtop  23879  xrsmopn  24981  nosupbnd1lem3  27885  nosupbnd1lem4  27886  noinfbnd1lem3  27900  noinfbnd1lem4  27901  noinfbnd1lem5  27902  precsexlem8  28418  bdayfinbndlem1  28671  axpasch  29302  axcontlem4  29328  elwwlks2ons3im  30314  mhmimasplusg  33366  br4  36258  btwnintr  36519  btwnexch3  36520  btwnouttr2  36522  cgrxfr  36555  lineext  36576  btwnconn1lem13  36599  btwnconn1lem14  36600  btwnconn3  36603  brsegle  36608  brsegle2  36609  segleantisym  36615  outsideofeu  36631  lineunray  36647  lineelsb2  36648  cvrcmp  40085  atcvrj2b  40234  3dimlem3  40263  3dimlem3OLDN  40264  3dim3  40271  ps-1  40279  lplnnle2at  40343  2llnm3N  40371  lvolnle3at  40384  4atlem0a  40395  4atlem3  40398  4atlem3a  40399  lnatexN  40581  paddasslem8  40629  paddasslem9  40630  paddasslem10  40631  paddasslem12  40633  paddasslem13  40634  lhp2lt  40803  lhpexle2lem  40811  lhpexle3  40814  lhpmcvr3  40827  lhpat3  40848  4atex  40878  trlval2  40965  ltrnideq  40977  ltrnatlw  40985  trlnle  40988  trlval4  40990  cdlemd4  41003  cdlemd5  41004  cdleme16  41087  cdleme21  41139  cdleme21k  41140  cdleme27cl  41168  cdleme27N  41171  cdleme29ex  41176  cdleme43fsv1snlem  41222  cdleme40m  41269  cdleme46f2g2  41295  cdleme46f2g1  41296  trlord  41371  cdlemg8  41433  cdlemg15a  41457  cdlemg16z  41461  cdlemg18a  41480  cdlemg24  41490  cdlemg38  41517  cdlemg40  41519  trlcone  41530  cdlemj2  41624  tendoid0  41627  tendoconid  41631  cdlemk34  41712  cdlemk38  41717  cdlemkid4  41736  cdlemk35s-id  41740  cdlemk39s-id  41742  cdlemk53  41759  tendospcanN  41825  cdlemm10N  41920  dihvalcqpre  42037  dihopelvalcpre  42050  dihord5b  42061  dihglblem5apreN  42093  dihmeetlem16N  42124  dihmeetlem17N  42125  dvh3dim3N  42251  qirropth  43663  mzpcong  43727  jm2.26  43757  aomclem6  43814  limcleqr  46386  fourierdlem42  46891  submodneaddmod  48122  itsclc0b  49580