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 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:  soisores  7264  frrlem4  8222  omopth2  8502  ttrcltr  9612  fin23lem11  10211  dedekind  11279  xaddass  13151  swrdsbslen  14571  swrdspsleq  14572  ntrivcvgmul  15809  pockthg  16818  gsumsgrpccat  18714  efgred  19627  decpmatmullem  22656  decpmatmul  22657  unconn  23314  basqtop  23596  utop2nei  24136  ucncn  24170  cxple2  26604  cxple2a  26606  nogesgn1ores  27584  nolt02o  27605  nogt01o  27606  nosupbnd1lem1  27618  nosupbnd1lem3  27620  nosupbnd1lem4  27621  nosupbnd1lem5  27622  noinfbnd1lem1  27633  noinfbnd1lem3  27635  noinfbnd1lem4  27636  noinfbnd1lem5  27637  noetalem1  27651  cofcut1  27833  ax5seglem1  28873  ax5seglem2  28874  axpasch  28886  axcontlem4  28912  1pthon2v  30097  mhmimasplusg  32993  cvmlift2lem10  35295  br4  35741  cgrcomim  35973  btwnintr  36003  btwnouttr2  36006  btwndiff  36011  btwnconn1lem14  36084  btwnconn3  36087  segcon2  36089  brsegle  36092  brsegle2  36093  segleantisym  36099  seglelin  36100  outsideofeu  36115  eqlkr  39088  eqlkr2  39089  lkrlsp  39091  atbtwn  39435  athgt  39445  3dimlem3  39450  3dimlem3OLDN  39451  3dim3  39458  3atlem7  39478  4atlem0a  39582  4atlem3a  39586  4atlem11  39598  lneq2at  39767  lnatexN  39768  cdlemb  39783  paddasslem6  39814  llnexchb2  39858  lhp2lt  39990  lhpexle2lem  39998  lhpexle3  40001  lhpmcvr3  40014  lhpat3  40035  ltrnnidn  40163  ltrneq3  40197  cdleme17b  40276  cdleme25a  40342  cdleme25dN  40345  cdleme27cl  40355  cdlemefrs29bpre0  40385  cdlemefs32sn1aw  40403  cdleme32le  40436  cdleme46f2g2  40482  cdleme46f2g1  40483  cdleme50trn3  40542  trlord  40558  ltrniotavalbN  40573  cdlemg6  40612  cdlemg7N  40615  cdlemg11b  40631  cdlemg15a  40644  cdlemg15  40645  cdlemg39  40705  trlcone  40717  cdlemg42  40718  tendoconid  40818  tendotr  40819  cdlemk39u  40957  cdlemk19u  40959  cdleml5N  40969  cdlemm10N  41107  dihord11b  41211  dihord2pre  41214  dihvalcqpre  41224  dihopelvalcpre  41237  dihord6apre  41245  dihord4  41247  dihord5b  41248  dihglblem5apreN  41280  dihmeetlem13N  41308  dihmeetlem19N  41314  dih1dimatlem0  41317  qirropth  42891  mzpcong  42955  jm2.25lem1  42981  jm2.26  42985  idomsubgmo  43176  fourierdlem42  46140  fourierdlem97  46194  clnbgrgrimlem  47927  line2  48747  itscnhlinecirc02plem2  48778