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  7838  omopth2  8551  ltmul1a  12038  xaddass  13216  xlemul2a  13256  swrdsbslen  14636  swrdspsleq  14637  dvdsadd2b  16283  pockthg  16884  psgnunilem4  19434  efgred  19685  ptbasin  23471  basqtop  23605  xrsmopn  24708  nosupbnd1lem3  27629  nosupbnd1lem4  27630  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  precsexlem8  28123  axpasch  28875  axcontlem4  28901  elwwlks2ons3im  29891  mhmimasplusg  32986  br4  35752  btwnintr  36014  btwnexch3  36015  btwnouttr2  36017  cgrxfr  36050  lineext  36071  btwnconn1lem13  36094  btwnconn1lem14  36095  btwnconn3  36098  brsegle  36103  brsegle2  36104  segleantisym  36110  outsideofeu  36126  lineunray  36142  lineelsb2  36143  cvrcmp  39283  atcvrj2b  39433  3dimlem3  39462  3dimlem3OLDN  39463  3dim3  39470  ps-1  39478  lplnnle2at  39542  2llnm3N  39570  lvolnle3at  39583  4atlem0a  39594  4atlem3  39597  4atlem3a  39598  lnatexN  39780  paddasslem8  39828  paddasslem9  39829  paddasslem10  39830  paddasslem12  39832  paddasslem13  39833  lhp2lt  40002  lhpexle2lem  40010  lhpexle3  40013  lhpmcvr3  40026  lhpat3  40047  4atex  40077  trlval2  40164  ltrnideq  40176  ltrnatlw  40184  trlnle  40187  trlval4  40189  cdlemd4  40202  cdlemd5  40203  cdleme16  40286  cdleme21  40338  cdleme21k  40339  cdleme27cl  40367  cdleme27N  40370  cdleme29ex  40375  cdleme43fsv1snlem  40421  cdleme40m  40468  cdleme46f2g2  40494  cdleme46f2g1  40495  trlord  40570  cdlemg8  40632  cdlemg15a  40656  cdlemg16z  40660  cdlemg18a  40679  cdlemg24  40689  cdlemg38  40716  cdlemg40  40718  trlcone  40729  cdlemj2  40823  tendoid0  40826  tendoconid  40830  cdlemk34  40911  cdlemk38  40916  cdlemkid4  40935  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk53  40958  tendospcanN  41024  cdlemm10N  41119  dihvalcqpre  41236  dihopelvalcpre  41249  dihord5b  41260  dihglblem5apreN  41292  dihmeetlem16N  41323  dihmeetlem17N  41324  dvh3dim3N  41450  qirropth  42903  mzpcong  42968  jm2.26  42998  aomclem6  43055  limcleqr  45649  fourierdlem42  46154  submodneaddmod  47356  itsclc0b  48765