Theorem simpl3l 1247

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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 402  df-3an 1105

This theorem is used by:  tfisi  7859  omopth2  8575  ltmul1a  12092  xaddass  13305  xlemul2a  13345  swrdsbslen  14738  swrdspsleq  14739  dvdsadd2b  16402  pockthg  17004  psgnunilem4  19630  efgred  19881  ptbasin  23809  basqtop  23943  xrsmopn  25045  nosupbnd1lem3  27954  nosupbnd1lem4  27955  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  precsexlem8  28487  bdayfinbndlem1  28740  axpasch  29406  axcontlem4  29432  elwwlks2ons3im  30430  mhmimasplusg  33485  br4  36345  btwnintr  36607  btwnexch3  36608  btwnouttr2  36610  cgrxfr  36643  lineext  36664  btwnconn1lem13  36687  btwnconn1lem14  36688  btwnconn3  36691  brsegle  36696  brsegle2  36697  segleantisym  36703  outsideofeu  36719  lineunray  36735  lineelsb2  36736  cvrcmp  40164  atcvrj2b  40313  3dimlem3  40342  3dimlem3OLDN  40343  3dim3  40350  ps-1  40358  lplnnle2at  40422  2llnm3N  40450  lvolnle3at  40463  4atlem0a  40474  4atlem3  40477  4atlem3a  40478  lnatexN  40660  paddasslem8  40708  paddasslem9  40709  paddasslem10  40710  paddasslem12  40712  paddasslem13  40713  lhp2lt  40882  lhpexle2lem  40890  lhpexle3  40893  lhpmcvr3  40906  lhpat3  40927  4atex  40957  trlval2  41044  ltrnideq  41056  ltrnatlw  41064  trlnle  41067  trlval4  41069  cdlemd4  41082  cdlemd5  41083  cdleme16  41166  cdleme21  41218  cdleme21k  41219  cdleme27cl  41247  cdleme27N  41250  cdleme29ex  41255  cdleme43fsv1snlem  41301  cdleme40m  41348  cdleme46f2g2  41374  cdleme46f2g1  41375  trlord  41450  cdlemg8  41512  cdlemg15a  41536  cdlemg16z  41540  cdlemg18a  41559  cdlemg24  41569  cdlemg38  41596  cdlemg40  41598  trlcone  41609  cdlemj2  41703  tendoid0  41706  tendoconid  41710  cdlemk34  41791  cdlemk38  41796  cdlemkid4  41815  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk53  41838  tendospcanN  41904  cdlemm10N  41999  dihvalcqpre  42116  dihopelvalcpre  42129  dihord5b  42140  dihglblem5apreN  42172  dihmeetlem16N  42203  dihmeetlem17N  42204  dvh3dim3N  42330  qirropth  43757  mzpcong  43821  jm2.26  43851  aomclem6  43908  limcleqr  46480  fourierdlem42  46985  submodneaddmod  48253  itsclc0b  49710