Theorem simpl3l 1228

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

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

This theorem is referenced by:  tfisi  7850  omopth2  8586  ltmul1a  12067  xaddass  13232  xlemul2a  13272  swrdsbslen  14618  swrdspsleq  14619  dvdsadd2b  16253  pockthg  16843  psgnunilem4  19406  efgred  19657  ptbasin  23301  basqtop  23435  xrsmopn  24548  nosupbnd1lem3  27437  nosupbnd1lem4  27438  noinfbnd1lem3  27452  noinfbnd1lem4  27453  noinfbnd1lem5  27454  precsexlem8  27887  axpasch  28454  axcontlem4  28480  elwwlks2ons3im  29463  mhmimasplusg  32454  br4  35020  btwnintr  35283  btwnexch3  35284  btwnouttr2  35286  cgrxfr  35319  lineext  35340  btwnconn1lem13  35363  btwnconn1lem14  35364  btwnconn3  35367  brsegle  35372  brsegle2  35373  segleantisym  35379  outsideofeu  35395  lineunray  35411  lineelsb2  35412  cvrcmp  38456  atcvrj2b  38606  3dimlem3  38635  3dimlem3OLDN  38636  3dim3  38643  ps-1  38651  lplnnle2at  38715  2llnm3N  38743  lvolnle3at  38756  4atlem0a  38767  4atlem3  38770  4atlem3a  38771  lnatexN  38953  paddasslem8  39001  paddasslem9  39002  paddasslem10  39003  paddasslem12  39005  paddasslem13  39006  lhp2lt  39175  lhpexle2lem  39183  lhpexle3  39186  lhpmcvr3  39199  lhpat3  39220  4atex  39250  trlval2  39337  ltrnideq  39349  ltrnatlw  39357  trlnle  39360  trlval4  39362  cdlemd4  39375  cdlemd5  39376  cdleme16  39459  cdleme21  39511  cdleme21k  39512  cdleme27cl  39540  cdleme27N  39543  cdleme29ex  39548  cdleme43fsv1snlem  39594  cdleme40m  39641  cdleme46f2g2  39667  cdleme46f2g1  39668  trlord  39743  cdlemg8  39805  cdlemg15a  39829  cdlemg16z  39833  cdlemg18a  39852  cdlemg24  39862  cdlemg38  39889  cdlemg40  39891  trlcone  39902  cdlemj2  39996  tendoid0  39999  tendoconid  40003  cdlemk34  40084  cdlemk38  40089  cdlemkid4  40108  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk53  40131  tendospcanN  40197  cdlemm10N  40292  dihvalcqpre  40409  dihopelvalcpre  40422  dihord5b  40433  dihglblem5apreN  40465  dihmeetlem16N  40496  dihmeetlem17N  40497  dvh3dim3N  40623  qirropth  41948  mzpcong  42013  jm2.26  42043  aomclem6  42103  limcleqr  44659  fourierdlem42  45164  itsclc0b  47546