Theorem simpl2l 1227

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  soisores  7324  frrlem4  8274  omopth2  8584  ttrcltr  9711  fin23lem11  10312  dedekind  11377  xaddass  13228  swrdsbslen  14614  swrdspsleq  14615  ntrivcvgmul  15848  pockthg  16839  gsumsgrpccat  18721  efgred  19616  decpmatmullem  22273  decpmatmul  22274  unconn  22933  basqtop  23215  utop2nei  23755  ucncn  23790  cxple2  26205  cxple2a  26207  nogesgn1ores  27177  nolt02o  27198  nogt01o  27199  nosupbnd1lem1  27211  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  noinfbnd1lem1  27226  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noetalem1  27244  cofcut1  27407  ax5seglem1  28186  ax5seglem2  28187  axpasch  28199  axcontlem4  28225  1pthon2v  29406  cvmlift2lem10  34303  br4  34728  cgrcomim  34961  btwnintr  34991  btwnouttr2  34994  btwndiff  34999  btwnconn1lem14  35072  btwnconn3  35075  segcon2  35077  brsegle  35080  brsegle2  35081  segleantisym  35087  seglelin  35088  outsideofeu  35103  eqlkr  37969  eqlkr2  37970  lkrlsp  37972  atbtwn  38317  athgt  38327  3dimlem3  38332  3dimlem3OLDN  38333  3dim3  38340  3atlem7  38360  4atlem0a  38464  4atlem3a  38468  4atlem11  38480  lneq2at  38649  lnatexN  38650  cdlemb  38665  paddasslem6  38696  llnexchb2  38740  lhp2lt  38872  lhpexle2lem  38880  lhpexle3  38883  lhpmcvr3  38896  lhpat3  38917  ltrnnidn  39045  ltrneq3  39079  cdleme17b  39158  cdleme25a  39224  cdleme25dN  39227  cdleme27cl  39237  cdlemefrs29bpre0  39267  cdlemefs32sn1aw  39285  cdleme32le  39318  cdleme46f2g2  39364  cdleme46f2g1  39365  cdleme50trn3  39424  trlord  39440  ltrniotavalbN  39455  cdlemg6  39494  cdlemg7N  39497  cdlemg11b  39513  cdlemg15a  39526  cdlemg15  39527  cdlemg39  39587  trlcone  39599  cdlemg42  39600  tendoconid  39700  tendotr  39701  cdlemk39u  39839  cdlemk19u  39841  cdleml5N  39851  cdlemm10N  39989  dihord11b  40093  dihord2pre  40096  dihvalcqpre  40106  dihopelvalcpre  40119  dihord6apre  40127  dihord4  40129  dihord5b  40130  dihglblem5apreN  40162  dihmeetlem13N  40190  dihmeetlem19N  40196  dih1dimatlem0  40199  qirropth  41646  mzpcong  41711  jm2.25lem1  41737  jm2.26  41741  idomsubgmo  41940  fourierdlem42  44865  fourierdlem97  44919  line2  47438  itscnhlinecirc02plem2  47469