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  7811  omopth2  8521  ltmul1a  12002  xaddass  13176  xlemul2a  13216  swrdsbslen  14600  swrdspsleq  14601  dvdsadd2b  16245  pockthg  16846  psgnunilem4  19438  efgred  19689  ptbasin  23533  basqtop  23667  xrsmopn  24769  nosupbnd1lem3  27690  nosupbnd1lem4  27691  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  precsexlem8  28222  bdayfinbndlem1  28475  axpasch  29026  axcontlem4  29052  elwwlks2ons3im  30039  mhmimasplusg  33130  br4  35971  btwnintr  36232  btwnexch3  36233  btwnouttr2  36235  cgrxfr  36268  lineext  36289  btwnconn1lem13  36312  btwnconn1lem14  36313  btwnconn3  36316  brsegle  36321  brsegle2  36322  segleantisym  36328  outsideofeu  36344  lineunray  36360  lineelsb2  36361  cvrcmp  39648  atcvrj2b  39797  3dimlem3  39826  3dimlem3OLDN  39827  3dim3  39834  ps-1  39842  lplnnle2at  39906  2llnm3N  39934  lvolnle3at  39947  4atlem0a  39958  4atlem3  39961  4atlem3a  39962  lnatexN  40144  paddasslem8  40192  paddasslem9  40193  paddasslem10  40194  paddasslem12  40196  paddasslem13  40197  lhp2lt  40366  lhpexle2lem  40374  lhpexle3  40377  lhpmcvr3  40390  lhpat3  40411  4atex  40441  trlval2  40528  ltrnideq  40540  ltrnatlw  40548  trlnle  40551  trlval4  40553  cdlemd4  40566  cdlemd5  40567  cdleme16  40650  cdleme21  40702  cdleme21k  40703  cdleme27cl  40731  cdleme27N  40734  cdleme29ex  40739  cdleme43fsv1snlem  40785  cdleme40m  40832  cdleme46f2g2  40858  cdleme46f2g1  40859  trlord  40934  cdlemg8  40996  cdlemg15a  41020  cdlemg16z  41024  cdlemg18a  41043  cdlemg24  41053  cdlemg38  41080  cdlemg40  41082  trlcone  41093  cdlemj2  41187  tendoid0  41190  tendoconid  41194  cdlemk34  41275  cdlemk38  41280  cdlemkid4  41299  cdlemk35s-id  41303  cdlemk39s-id  41305  cdlemk53  41322  tendospcanN  41388  cdlemm10N  41483  dihvalcqpre  41600  dihopelvalcpre  41613  dihord5b  41624  dihglblem5apreN  41656  dihmeetlem16N  41687  dihmeetlem17N  41688  dvh3dim3N  41814  qirropth  43254  mzpcong  43318  jm2.26  43348  aomclem6  43405  limcleqr  45991  fourierdlem42  46496  submodneaddmod  47700  itsclc0b  49121