Theorem simpl3l 1245

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  tfisi  7843  omopth2  8557  ltmul1a  12055  xaddass  13266  xlemul2a  13306  swrdsbslen  14692  swrdspsleq  14693  dvdsadd2b  16354  pockthg  16956  psgnunilem4  19558  efgred  19809  ptbasin  23695  basqtop  23829  xrsmopn  24931  nosupbnd1lem3  27832  nosupbnd1lem4  27833  noinfbnd1lem3  27847  noinfbnd1lem4  27848  noinfbnd1lem5  27849  precsexlem8  28365  bdayfinbndlem1  28618  axpasch  29200  axcontlem4  29226  elwwlks2ons3im  30212  mhmimasplusg  33270  br4  36121  btwnintr  36382  btwnexch3  36383  btwnouttr2  36385  cgrxfr  36418  lineext  36439  btwnconn1lem13  36462  btwnconn1lem14  36463  btwnconn3  36466  brsegle  36471  brsegle2  36472  segleantisym  36478  outsideofeu  36494  lineunray  36510  lineelsb2  36511  cvrcmp  39919  atcvrj2b  40068  3dimlem3  40097  3dimlem3OLDN  40098  3dim3  40105  ps-1  40113  lplnnle2at  40177  2llnm3N  40205  lvolnle3at  40218  4atlem0a  40229  4atlem3  40232  4atlem3a  40233  lnatexN  40415  paddasslem8  40463  paddasslem9  40464  paddasslem10  40465  paddasslem12  40467  paddasslem13  40468  lhp2lt  40637  lhpexle2lem  40645  lhpexle3  40648  lhpmcvr3  40661  lhpat3  40682  4atex  40712  trlval2  40799  ltrnideq  40811  ltrnatlw  40819  trlnle  40822  trlval4  40824  cdlemd4  40837  cdlemd5  40838  cdleme16  40921  cdleme21  40973  cdleme21k  40974  cdleme27cl  41002  cdleme27N  41005  cdleme29ex  41010  cdleme43fsv1snlem  41056  cdleme40m  41103  cdleme46f2g2  41129  cdleme46f2g1  41130  trlord  41205  cdlemg8  41267  cdlemg15a  41291  cdlemg16z  41295  cdlemg18a  41314  cdlemg24  41324  cdlemg38  41351  cdlemg40  41353  trlcone  41364  cdlemj2  41458  tendoid0  41461  tendoconid  41465  cdlemk34  41546  cdlemk38  41551  cdlemkid4  41570  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk53  41593  tendospcanN  41659  cdlemm10N  41754  dihvalcqpre  41871  dihopelvalcpre  41884  dihord5b  41895  dihglblem5apreN  41927  dihmeetlem16N  41958  dihmeetlem17N  41959  dvh3dim3N  42085  qirropth  43497  mzpcong  43561  jm2.26  43591  aomclem6  43648  limcleqr  46216  fourierdlem42  46721  submodneaddmod  47949  itsclc0b  49403