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  7858  omopth2  8574  ltmul1a  12091  xaddass  13303  xlemul2a  13343  swrdsbslen  14736  swrdspsleq  14737  dvdsadd2b  16400  pockthg  17002  psgnunilem4  19628  efgred  19879  ptbasin  23807  basqtop  23941  xrsmopn  25043  nosupbnd1lem3  27947  nosupbnd1lem4  27948  noinfbnd1lem3  27962  noinfbnd1lem4  27963  noinfbnd1lem5  27964  precsexlem8  28480  bdayfinbndlem1  28733  axpasch  29399  axcontlem4  29425  elwwlks2ons3im  30423  mhmimasplusg  33479  br4  36339  btwnintr  36601  btwnexch3  36602  btwnouttr2  36604  cgrxfr  36637  lineext  36658  btwnconn1lem13  36681  btwnconn1lem14  36682  btwnconn3  36685  brsegle  36690  brsegle2  36691  segleantisym  36697  outsideofeu  36713  lineunray  36729  lineelsb2  36730  cvrcmp  40158  atcvrj2b  40307  3dimlem3  40336  3dimlem3OLDN  40337  3dim3  40344  ps-1  40352  lplnnle2at  40416  2llnm3N  40444  lvolnle3at  40457  4atlem0a  40468  4atlem3  40471  4atlem3a  40472  lnatexN  40654  paddasslem8  40702  paddasslem9  40703  paddasslem10  40704  paddasslem12  40706  paddasslem13  40707  lhp2lt  40876  lhpexle2lem  40884  lhpexle3  40887  lhpmcvr3  40900  lhpat3  40921  4atex  40951  trlval2  41038  ltrnideq  41050  ltrnatlw  41058  trlnle  41061  trlval4  41063  cdlemd4  41076  cdlemd5  41077  cdleme16  41160  cdleme21  41212  cdleme21k  41213  cdleme27cl  41241  cdleme27N  41244  cdleme29ex  41249  cdleme43fsv1snlem  41295  cdleme40m  41342  cdleme46f2g2  41368  cdleme46f2g1  41369  trlord  41444  cdlemg8  41506  cdlemg15a  41530  cdlemg16z  41534  cdlemg18a  41553  cdlemg24  41563  cdlemg38  41590  cdlemg40  41592  trlcone  41603  cdlemj2  41697  tendoid0  41700  tendoconid  41704  cdlemk34  41785  cdlemk38  41790  cdlemkid4  41809  cdlemk35s-id  41813  cdlemk39s-id  41815  cdlemk53  41832  tendospcanN  41898  cdlemm10N  41993  dihvalcqpre  42110  dihopelvalcpre  42123  dihord5b  42134  dihglblem5apreN  42166  dihmeetlem16N  42197  dihmeetlem17N  42198  dvh3dim3N  42324  qirropth  43751  mzpcong  43815  jm2.26  43845  aomclem6  43902  limcleqr  46474  fourierdlem42  46979  submodneaddmod  48247  itsclc0b  49704