Theorem simpl2l 1228

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

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

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 1089

This theorem is referenced by:  soisores  7275  frrlem4  8232  omopth2  8512  ttrcltr  9628  fin23lem11  10230  dedekind  11300  xaddass  13192  swrdsbslen  14618  swrdspsleq  14619  ntrivcvgmul  15858  pockthg  16868  gsumsgrpccat  18799  efgred  19714  decpmatmullem  22746  decpmatmul  22747  unconn  23404  basqtop  23686  utop2nei  24225  ucncn  24259  cxple2  26674  cxple2a  26676  nogesgn1ores  27652  nolt02o  27673  nogt01o  27674  nosupbnd1lem1  27686  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  noinfbnd1lem1  27701  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noetalem1  27719  cofcut1  27926  bdayfinbndlem1  28473  ax5seglem1  29011  ax5seglem2  29012  axpasch  29024  axcontlem4  29050  1pthon2v  30238  mhmimasplusg  33113  cvmlift2lem10  35510  br4  35956  cgrcomim  36187  btwnintr  36217  btwnouttr2  36220  btwndiff  36225  btwnconn1lem14  36298  btwnconn3  36301  segcon2  36303  brsegle  36306  brsegle2  36307  segleantisym  36313  seglelin  36314  outsideofeu  36329  eqlkr  39559  eqlkr2  39560  lkrlsp  39562  atbtwn  39906  athgt  39916  3dimlem3  39921  3dimlem3OLDN  39922  3dim3  39929  3atlem7  39949  4atlem0a  40053  4atlem3a  40057  4atlem11  40069  lneq2at  40238  lnatexN  40239  cdlemb  40254  paddasslem6  40285  llnexchb2  40329  lhp2lt  40461  lhpexle2lem  40469  lhpexle3  40472  lhpmcvr3  40485  lhpat3  40506  ltrnnidn  40634  ltrneq3  40668  cdleme17b  40747  cdleme25a  40813  cdleme25dN  40816  cdleme27cl  40826  cdlemefrs29bpre0  40856  cdlemefs32sn1aw  40874  cdleme32le  40907  cdleme46f2g2  40953  cdleme46f2g1  40954  cdleme50trn3  41013  trlord  41029  ltrniotavalbN  41044  cdlemg6  41083  cdlemg7N  41086  cdlemg11b  41102  cdlemg15a  41115  cdlemg15  41116  cdlemg39  41176  trlcone  41188  cdlemg42  41189  tendoconid  41289  tendotr  41290  cdlemk39u  41428  cdlemk19u  41430  cdleml5N  41440  cdlemm10N  41578  dihord11b  41682  dihord2pre  41685  dihvalcqpre  41695  dihopelvalcpre  41708  dihord6apre  41716  dihord4  41718  dihord5b  41719  dihglblem5apreN  41751  dihmeetlem13N  41779  dihmeetlem19N  41785  dih1dimatlem0  41788  qirropth  43354  mzpcong  43418  jm2.25lem1  43444  jm2.26  43448  idomsubgmo  43639  fourierdlem42  46595  fourierdlem97  46649  clnbgrgrimlem  48421  line2  49240  itscnhlinecirc02plem2  49271