Theorem simpl2l 1206

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  soisores  6901  omopth2  8007  fin23lem11  9533  dedekind  10599  xaddass  12455  swrdsbslen  13835  swrdspsleq  13836  ntrivcvgmul  15112  pockthg  16092  gsmsymgreqlem2  18314  efgred  18628  decpmatmullem  21077  decpmatmul  21078  unconn  21735  basqtop  22017  utop2nei  22556  ucncn  22591  cxple2  24975  cxple2a  24977  ax5seglem1  26411  ax5seglem2  26412  axpasch  26424  axcontlem4  26450  1pthon2v  27676  cvmlift2lem10  32134  br4  32484  frrlem4  32617  nolt02o  32690  nosupbnd1lem1  32699  nosupbnd1lem3  32701  nosupbnd1lem4  32702  nosupbnd1lem5  32703  cgrcomim  32941  btwnintr  32971  btwnouttr2  32974  btwndiff  32979  btwnconn1lem14  33052  btwnconn3  33055  segcon2  33057  brsegle  33060  brsegle2  33061  segleantisym  33067  seglelin  33068  outsideofeu  33083  eqlkr  35658  eqlkr2  35659  lkrlsp  35661  atbtwn  36005  athgt  36015  3dimlem3  36020  3dimlem3OLDN  36021  3dim3  36028  3atlem7  36048  4atlem0a  36152  4atlem3a  36156  4atlem11  36168  lneq2at  36337  lnatexN  36338  cdlemb  36353  paddasslem6  36384  llnexchb2  36428  lhp2lt  36560  lhpexle2lem  36568  lhpexle3  36571  lhpmcvr3  36584  lhpat3  36605  ltrnnidn  36733  ltrneq3  36767  cdleme17b  36846  cdleme25a  36912  cdleme25dN  36915  cdleme27cl  36925  cdlemefrs29bpre0  36955  cdlemefs32sn1aw  36973  cdleme32le  37006  cdleme46f2g2  37052  cdleme46f2g1  37053  cdleme50trn3  37112  trlord  37128  ltrniotavalbN  37143  cdlemg6  37182  cdlemg7N  37185  cdlemg11b  37201  cdlemg15a  37214  cdlemg15  37215  cdlemg39  37275  trlcone  37287  cdlemg42  37288  tendoconid  37388  tendotr  37389  cdlemk39u  37527  cdlemk19u  37529  cdleml5N  37539  cdlemm10N  37677  dihord11b  37781  dihord2pre  37784  dihvalcqpre  37794  dihopelvalcpre  37807  dihord6apre  37815  dihord4  37817  dihord5b  37818  dihglblem5apreN  37850  dihmeetlem13N  37878  dihmeetlem19N  37884  dih1dimatlem0  37887  qirropth  38879  mzpcong  38943  jm2.25lem1  38969  jm2.26  38973  idomsubgmo  39172  fourierdlem42  41844  fourierdlem97  41898  line2  44081  itscnhlinecirc02plem2  44112