Theorem simpl3l 1229

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  tfisi  7593  omopth2  8242  ltmul1a  11568  xaddass  12726  xlemul2a  12766  swrdsbslen  14116  swrdspsleq  14117  dvdsadd2b  15752  pockthg  16343  psgnunilem4  18744  efgred  18993  ptbasin  22329  basqtop  22463  xrsmopn  23565  axpasch  26887  axcontlem4  26913  elwwlks2ons3im  27892  br4  33297  nosupbnd1lem3  33554  nosupbnd1lem4  33555  noinfbnd1lem3  33569  noinfbnd1lem4  33570  noinfbnd1lem5  33571  btwnintr  33959  btwnexch3  33960  btwnouttr2  33962  cgrxfr  33995  lineext  34016  btwnconn1lem13  34039  btwnconn1lem14  34040  btwnconn3  34043  brsegle  34048  brsegle2  34049  segleantisym  34055  outsideofeu  34071  lineunray  34087  lineelsb2  34088  cvrcmp  36917  atcvrj2b  37066  3dimlem3  37095  3dimlem3OLDN  37096  3dim3  37103  ps-1  37111  lplnnle2at  37175  2llnm3N  37203  lvolnle3at  37216  4atlem0a  37227  4atlem3  37230  4atlem3a  37231  lnatexN  37413  paddasslem8  37461  paddasslem9  37462  paddasslem10  37463  paddasslem12  37465  paddasslem13  37466  lhp2lt  37635  lhpexle2lem  37643  lhpexle3  37646  lhpmcvr3  37659  lhpat3  37680  4atex  37710  trlval2  37797  ltrnideq  37809  ltrnatlw  37817  trlnle  37820  trlval4  37822  cdlemd4  37835  cdlemd5  37836  cdleme16  37919  cdleme21  37971  cdleme21k  37972  cdleme27cl  38000  cdleme27N  38003  cdleme29ex  38008  cdleme43fsv1snlem  38054  cdleme40m  38101  cdleme46f2g2  38127  cdleme46f2g1  38128  trlord  38203  cdlemg8  38265  cdlemg15a  38289  cdlemg16z  38293  cdlemg18a  38312  cdlemg24  38322  cdlemg38  38349  cdlemg40  38351  trlcone  38362  cdlemj2  38456  tendoid0  38459  tendoconid  38463  cdlemk34  38544  cdlemk38  38549  cdlemkid4  38568  cdlemk35s-id  38572  cdlemk39s-id  38574  cdlemk53  38591  tendospcanN  38657  cdlemm10N  38752  dihvalcqpre  38869  dihopelvalcpre  38882  dihord5b  38893  dihglblem5apreN  38925  dihmeetlem16N  38956  dihmeetlem17N  38957  dvh3dim3N  39083  qirropth  40294  mzpcong  40358  jm2.26  40388  aomclem6  40448  limcleqr  42719  fourierdlem42  43224  itsclc0b  45644