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  7273  frrlem4  8231  omopth2  8511  ttrcltr  9625  fin23lem11  10227  dedekind  11296  xaddass  13164  swrdsbslen  14588  swrdspsleq  14589  ntrivcvgmul  15825  pockthg  16834  gsumsgrpccat  18765  efgred  19677  decpmatmullem  22715  decpmatmul  22716  unconn  23373  basqtop  23655  utop2nei  24194  ucncn  24228  cxple2  26662  cxple2a  26664  nogesgn1ores  27642  nolt02o  27663  nogt01o  27664  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  noinfbnd1lem1  27691  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noetalem1  27709  cofcut1  27916  bdayfinbndlem1  28463  ax5seglem1  29001  ax5seglem2  29002  axpasch  29014  axcontlem4  29040  1pthon2v  30228  mhmimasplusg  33120  cvmlift2lem10  35506  br4  35952  cgrcomim  36183  btwnintr  36213  btwnouttr2  36216  btwndiff  36221  btwnconn1lem14  36294  btwnconn3  36297  segcon2  36299  brsegle  36302  brsegle2  36303  segleantisym  36309  seglelin  36310  outsideofeu  36325  eqlkr  39355  eqlkr2  39356  lkrlsp  39358  atbtwn  39702  athgt  39712  3dimlem3  39717  3dimlem3OLDN  39718  3dim3  39725  3atlem7  39745  4atlem0a  39849  4atlem3a  39853  4atlem11  39865  lneq2at  40034  lnatexN  40035  cdlemb  40050  paddasslem6  40081  llnexchb2  40125  lhp2lt  40257  lhpexle2lem  40265  lhpexle3  40268  lhpmcvr3  40281  lhpat3  40302  ltrnnidn  40430  ltrneq3  40464  cdleme17b  40543  cdleme25a  40609  cdleme25dN  40612  cdleme27cl  40622  cdlemefrs29bpre0  40652  cdlemefs32sn1aw  40670  cdleme32le  40703  cdleme46f2g2  40749  cdleme46f2g1  40750  cdleme50trn3  40809  trlord  40825  ltrniotavalbN  40840  cdlemg6  40879  cdlemg7N  40882  cdlemg11b  40898  cdlemg15a  40911  cdlemg15  40912  cdlemg39  40972  trlcone  40984  cdlemg42  40985  tendoconid  41085  tendotr  41086  cdlemk39u  41224  cdlemk19u  41226  cdleml5N  41236  cdlemm10N  41374  dihord11b  41478  dihord2pre  41481  dihvalcqpre  41491  dihopelvalcpre  41504  dihord6apre  41512  dihord4  41514  dihord5b  41515  dihglblem5apreN  41547  dihmeetlem13N  41575  dihmeetlem19N  41581  dih1dimatlem0  41584  qirropth  43146  mzpcong  43210  jm2.25lem1  43236  jm2.26  43240  idomsubgmo  43431  fourierdlem42  46389  fourierdlem97  46443  clnbgrgrimlem  48175  line2  48994  itscnhlinecirc02plem2  49025