Theorem simpl3l 1229

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl3l	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl3l

Step	Hyp	Ref	Expression
1		simpll 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1188	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:  tfisi  7854  omopth2  8596  ltmul1a  12090  xaddass  13265  xlemul2a  13305  swrdsbslen  14682  swrdspsleq  14683  dvdsadd2b  16325  pockthg  16926  psgnunilem4  19478  efgred  19729  ptbasin  23515  basqtop  23649  xrsmopn  24752  nosupbnd1lem3  27674  nosupbnd1lem4  27675  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  precsexlem8  28168  axpasch  28920  axcontlem4  28946  elwwlks2ons3im  29936  mhmimasplusg  33033  br4  35775  btwnintr  36037  btwnexch3  36038  btwnouttr2  36040  cgrxfr  36073  lineext  36094  btwnconn1lem13  36117  btwnconn1lem14  36118  btwnconn3  36121  brsegle  36126  brsegle2  36127  segleantisym  36133  outsideofeu  36149  lineunray  36165  lineelsb2  36166  cvrcmp  39301  atcvrj2b  39451  3dimlem3  39480  3dimlem3OLDN  39481  3dim3  39488  ps-1  39496  lplnnle2at  39560  2llnm3N  39588  lvolnle3at  39601  4atlem0a  39612  4atlem3  39615  4atlem3a  39616  lnatexN  39798  paddasslem8  39846  paddasslem9  39847  paddasslem10  39848  paddasslem12  39850  paddasslem13  39851  lhp2lt  40020  lhpexle2lem  40028  lhpexle3  40031  lhpmcvr3  40044  lhpat3  40065  4atex  40095  trlval2  40182  ltrnideq  40194  ltrnatlw  40202  trlnle  40205  trlval4  40207  cdlemd4  40220  cdlemd5  40221  cdleme16  40304  cdleme21  40356  cdleme21k  40357  cdleme27cl  40385  cdleme27N  40388  cdleme29ex  40393  cdleme43fsv1snlem  40439  cdleme40m  40486  cdleme46f2g2  40512  cdleme46f2g1  40513  trlord  40588  cdlemg8  40650  cdlemg15a  40674  cdlemg16z  40678  cdlemg18a  40697  cdlemg24  40707  cdlemg38  40734  cdlemg40  40736  trlcone  40747  cdlemj2  40841  tendoid0  40844  tendoconid  40848  cdlemk34  40929  cdlemk38  40934  cdlemkid4  40953  cdlemk35s-id  40957  cdlemk39s-id  40959  cdlemk53  40976  tendospcanN  41042  cdlemm10N  41137  dihvalcqpre  41254  dihopelvalcpre  41267  dihord5b  41278  dihglblem5apreN  41310  dihmeetlem16N  41341  dihmeetlem17N  41342  dvh3dim3N  41468  qirropth  42931  mzpcong  42996  jm2.26  43026  aomclem6  43083  limcleqr  45673  fourierdlem42  46178  submodneaddmod  47380  itsclc0b  48752