Theorem simpl2l 1223

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl2l	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl2l

Step	Hyp	Ref	Expression
1		simpll 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl2 1183	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  soisores  7331  frrlem4  8296  omopth2  8606  ttrcltr  9752  fin23lem11  10351  dedekind  11418  xaddass  13276  swrdsbslen  14667  swrdspsleq  14668  ntrivcvgmul  15901  pockthg  16903  gsumsgrpccat  18825  efgred  19742  decpmatmullem  22761  decpmatmul  22762  unconn  23421  basqtop  23703  utop2nei  24243  ucncn  24278  cxple2  26721  cxple2a  26723  nogesgn1ores  27701  nolt02o  27722  nogt01o  27723  nosupbnd1lem1  27735  nosupbnd1lem3  27737  nosupbnd1lem4  27738  nosupbnd1lem5  27739  noinfbnd1lem1  27750  noinfbnd1lem3  27752  noinfbnd1lem4  27753  noinfbnd1lem5  27754  noetalem1  27768  cofcut1  27934  ax5seglem1  28859  ax5seglem2  28860  axpasch  28872  axcontlem4  28898  1pthon2v  30083  mhmimasplusg  32914  cvmlift2lem10  35153  br4  35593  cgrcomim  35826  btwnintr  35856  btwnouttr2  35859  btwndiff  35864  btwnconn1lem14  35937  btwnconn3  35940  segcon2  35942  brsegle  35945  brsegle2  35946  segleantisym  35952  seglelin  35953  outsideofeu  35968  eqlkr  38810  eqlkr2  38811  lkrlsp  38813  atbtwn  39158  athgt  39168  3dimlem3  39173  3dimlem3OLDN  39174  3dim3  39181  3atlem7  39201  4atlem0a  39305  4atlem3a  39309  4atlem11  39321  lneq2at  39490  lnatexN  39491  cdlemb  39506  paddasslem6  39537  llnexchb2  39581  lhp2lt  39713  lhpexle2lem  39721  lhpexle3  39724  lhpmcvr3  39737  lhpat3  39758  ltrnnidn  39886  ltrneq3  39920  cdleme17b  39999  cdleme25a  40065  cdleme25dN  40068  cdleme27cl  40078  cdlemefrs29bpre0  40108  cdlemefs32sn1aw  40126  cdleme32le  40159  cdleme46f2g2  40205  cdleme46f2g1  40206  cdleme50trn3  40265  trlord  40281  ltrniotavalbN  40296  cdlemg6  40335  cdlemg7N  40338  cdlemg11b  40354  cdlemg15a  40367  cdlemg15  40368  cdlemg39  40428  trlcone  40440  cdlemg42  40441  tendoconid  40541  tendotr  40542  cdlemk39u  40680  cdlemk19u  40682  cdleml5N  40692  cdlemm10N  40830  dihord11b  40934  dihord2pre  40937  dihvalcqpre  40947  dihopelvalcpre  40960  dihord6apre  40968  dihord4  40970  dihord5b  40971  dihglblem5apreN  41003  dihmeetlem13N  41031  dihmeetlem19N  41037  dih1dimatlem0  41040  qirropth  42602  mzpcong  42667  jm2.25lem1  42693  jm2.26  42697  idomsubgmo  42895  fourierdlem42  45806  fourierdlem97  45860  clnbgrgrimlem  47516  line2  48176  itscnhlinecirc02plem2  48207