Theorem simpl3l 1229

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  tfisi  7835  omopth2  8548  ltmul1a  12031  xaddass  13209  xlemul2a  13249  swrdsbslen  14629  swrdspsleq  14630  dvdsadd2b  16276  pockthg  16877  psgnunilem4  19427  efgred  19678  ptbasin  23464  basqtop  23598  xrsmopn  24701  nosupbnd1lem3  27622  nosupbnd1lem4  27623  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  precsexlem8  28116  axpasch  28868  axcontlem4  28894  elwwlks2ons3im  29884  mhmimasplusg  32979  br4  35745  btwnintr  36007  btwnexch3  36008  btwnouttr2  36010  cgrxfr  36043  lineext  36064  btwnconn1lem13  36087  btwnconn1lem14  36088  btwnconn3  36091  brsegle  36096  brsegle2  36097  segleantisym  36103  outsideofeu  36119  lineunray  36135  lineelsb2  36136  cvrcmp  39276  atcvrj2b  39426  3dimlem3  39455  3dimlem3OLDN  39456  3dim3  39463  ps-1  39471  lplnnle2at  39535  2llnm3N  39563  lvolnle3at  39576  4atlem0a  39587  4atlem3  39590  4atlem3a  39591  lnatexN  39773  paddasslem8  39821  paddasslem9  39822  paddasslem10  39823  paddasslem12  39825  paddasslem13  39826  lhp2lt  39995  lhpexle2lem  40003  lhpexle3  40006  lhpmcvr3  40019  lhpat3  40040  4atex  40070  trlval2  40157  ltrnideq  40169  ltrnatlw  40177  trlnle  40180  trlval4  40182  cdlemd4  40195  cdlemd5  40196  cdleme16  40279  cdleme21  40331  cdleme21k  40332  cdleme27cl  40360  cdleme27N  40363  cdleme29ex  40368  cdleme43fsv1snlem  40414  cdleme40m  40461  cdleme46f2g2  40487  cdleme46f2g1  40488  trlord  40563  cdlemg8  40625  cdlemg15a  40649  cdlemg16z  40653  cdlemg18a  40672  cdlemg24  40682  cdlemg38  40709  cdlemg40  40711  trlcone  40722  cdlemj2  40816  tendoid0  40819  tendoconid  40823  cdlemk34  40904  cdlemk38  40909  cdlemkid4  40928  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk53  40951  tendospcanN  41017  cdlemm10N  41112  dihvalcqpre  41229  dihopelvalcpre  41242  dihord5b  41253  dihglblem5apreN  41285  dihmeetlem16N  41316  dihmeetlem17N  41317  dvh3dim3N  41443  qirropth  42896  mzpcong  42961  jm2.26  42991  aomclem6  43048  limcleqr  45642  fourierdlem42  46147  submodneaddmod  47352  itsclc0b  48761