Theorem simpl3l 1247

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 779	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1206	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfisi  7894  omopth2  8620  ltmul1a  12193  xaddass  13406  xlemul2a  13446  swrdsbslen  14842  swrdspsleq  14843  dvdsadd2b  16505  pockthg  17113  psgnunilem4  19741  efgred  19992  ptbasin  23926  basqtop  24060  xrsmopn  25162  nosupbnd1lem3  28097  nosupbnd1lem4  28098  noinfbnd1lem3  28112  noinfbnd1lem4  28113  noinfbnd1lem5  28114  precsexlem8  28630  bdayfinbndlem1  28883  axpasch  29549  axcontlem4  29575  elwwlks2ons3im  30573  mhmimasplusg  33668  br4  36701  btwnintr  36962  btwnexch3  36963  btwnouttr2  36965  cgrxfr  36998  lineext  37019  btwnconn1lem13  37042  btwnconn1lem14  37043  btwnconn3  37046  brsegle  37051  brsegle2  37052  segleantisym  37058  outsideofeu  37074  lineunray  37090  lineelsb2  37091  cvrcmp  40532  atcvrj2b  40681  3dimlem3  40710  3dimlem3OLDN  40711  3dim3  40718  ps-1  40726  lplnnle2at  40790  2llnm3N  40818  lvolnle3at  40831  4atlem0a  40842  4atlem3  40845  4atlem3a  40846  lnatexN  41028  paddasslem8  41076  paddasslem9  41077  paddasslem10  41078  paddasslem12  41080  paddasslem13  41081  lhp2lt  41250  lhpexle2lem  41258  lhpexle3  41261  lhpmcvr3  41274  lhpat3  41295  4atex  41325  trlval2  41412  ltrnideq  41424  ltrnatlw  41432  trlnle  41435  trlval4  41437  cdlemd4  41450  cdlemd5  41451  cdleme16  41534  cdleme21  41586  cdleme21k  41587  cdleme27cl  41615  cdleme27N  41618  cdleme29ex  41623  cdleme43fsv1snlem  41669  cdleme40m  41716  cdleme46f2g2  41742  cdleme46f2g1  41743  trlord  41818  cdlemg8  41880  cdlemg15a  41904  cdlemg16z  41908  cdlemg18a  41927  cdlemg24  41937  cdlemg38  41964  cdlemg40  41966  trlcone  41977  cdlemj2  42071  tendoid0  42074  tendoconid  42078  cdlemk34  42159  cdlemk38  42164  cdlemkid4  42183  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk53  42206  tendospcanN  42272  cdlemm10N  42367  dihvalcqpre  42484  dihopelvalcpre  42497  dihord5b  42508  dihglblem5apreN  42540  dihmeetlem16N  42571  dihmeetlem17N  42572  dvh3dim3N  42698  qirropth  44108  mzpcong  44172  jm2.26  44202  aomclem6  44254  limcleqr  46859  fourierdlem42  47364  submodneaddmod  48632  itsclc0b  50089