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  7853  omopth2  8570  ltmul1a  12136  xaddass  13349  xlemul2a  13389  swrdsbslen  14782  swrdspsleq  14783  dvdsadd2b  16444  pockthg  17046  psgnunilem4  19673  efgred  19924  ptbasin  23858  basqtop  23992  xrsmopn  25094  nosupbnd1lem3  28001  nosupbnd1lem4  28002  noinfbnd1lem3  28016  noinfbnd1lem4  28017  noinfbnd1lem5  28018  precsexlem8  28534  bdayfinbndlem1  28787  axpasch  29453  axcontlem4  29479  elwwlks2ons3im  30477  mhmimasplusg  33532  br4  36444  btwnintr  36706  btwnexch3  36707  btwnouttr2  36709  cgrxfr  36742  lineext  36763  btwnconn1lem13  36786  btwnconn1lem14  36787  btwnconn3  36790  brsegle  36795  brsegle2  36796  segleantisym  36802  outsideofeu  36818  lineunray  36834  lineelsb2  36835  cvrcmp  40260  atcvrj2b  40409  3dimlem3  40438  3dimlem3OLDN  40439  3dim3  40446  ps-1  40454  lplnnle2at  40518  2llnm3N  40546  lvolnle3at  40559  4atlem0a  40570  4atlem3  40573  4atlem3a  40574  lnatexN  40756  paddasslem8  40804  paddasslem9  40805  paddasslem10  40806  paddasslem12  40808  paddasslem13  40809  lhp2lt  40978  lhpexle2lem  40986  lhpexle3  40989  lhpmcvr3  41002  lhpat3  41023  4atex  41053  trlval2  41140  ltrnideq  41152  ltrnatlw  41160  trlnle  41163  trlval4  41165  cdlemd4  41178  cdlemd5  41179  cdleme16  41262  cdleme21  41314  cdleme21k  41315  cdleme27cl  41343  cdleme27N  41346  cdleme29ex  41351  cdleme43fsv1snlem  41397  cdleme40m  41444  cdleme46f2g2  41470  cdleme46f2g1  41471  trlord  41546  cdlemg8  41608  cdlemg15a  41632  cdlemg16z  41636  cdlemg18a  41655  cdlemg24  41665  cdlemg38  41692  cdlemg40  41694  trlcone  41705  cdlemj2  41799  tendoid0  41802  tendoconid  41806  cdlemk34  41887  cdlemk38  41892  cdlemkid4  41911  cdlemk35s-id  41915  cdlemk39s-id  41917  cdlemk53  41934  tendospcanN  42000  cdlemm10N  42095  dihvalcqpre  42212  dihopelvalcpre  42225  dihord5b  42236  dihglblem5apreN  42268  dihmeetlem16N  42299  dihmeetlem17N  42300  dvh3dim3N  42426  qirropth  43853  mzpcong  43917  jm2.26  43947  aomclem6  44004  limcleqr  46576  fourierdlem42  47081  submodneaddmod  48349  itsclc0b  49806