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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  tfisi  7880  omopth2  8622  ltmul1a  12116  xaddass  13291  xlemul2a  13331  swrdsbslen  14702  swrdspsleq  14703  dvdsadd2b  16343  pockthg  16944  psgnunilem4  19515  efgred  19766  ptbasin  23585  basqtop  23719  xrsmopn  24834  nosupbnd1lem3  27755  nosupbnd1lem4  27756  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  precsexlem8  28238  axpasch  28956  axcontlem4  28982  elwwlks2ons3im  29974  mhmimasplusg  33043  br4  35758  btwnintr  36020  btwnexch3  36021  btwnouttr2  36023  cgrxfr  36056  lineext  36077  btwnconn1lem13  36100  btwnconn1lem14  36101  btwnconn3  36104  brsegle  36109  brsegle2  36110  segleantisym  36116  outsideofeu  36132  lineunray  36148  lineelsb2  36149  cvrcmp  39284  atcvrj2b  39434  3dimlem3  39463  3dimlem3OLDN  39464  3dim3  39471  ps-1  39479  lplnnle2at  39543  2llnm3N  39571  lvolnle3at  39584  4atlem0a  39595  4atlem3  39598  4atlem3a  39599  lnatexN  39781  paddasslem8  39829  paddasslem9  39830  paddasslem10  39831  paddasslem12  39833  paddasslem13  39834  lhp2lt  40003  lhpexle2lem  40011  lhpexle3  40014  lhpmcvr3  40027  lhpat3  40048  4atex  40078  trlval2  40165  ltrnideq  40177  ltrnatlw  40185  trlnle  40188  trlval4  40190  cdlemd4  40203  cdlemd5  40204  cdleme16  40287  cdleme21  40339  cdleme21k  40340  cdleme27cl  40368  cdleme27N  40371  cdleme29ex  40376  cdleme43fsv1snlem  40422  cdleme40m  40469  cdleme46f2g2  40495  cdleme46f2g1  40496  trlord  40571  cdlemg8  40633  cdlemg15a  40657  cdlemg16z  40661  cdlemg18a  40680  cdlemg24  40690  cdlemg38  40717  cdlemg40  40719  trlcone  40730  cdlemj2  40824  tendoid0  40827  tendoconid  40831  cdlemk34  40912  cdlemk38  40917  cdlemkid4  40936  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk53  40959  tendospcanN  41025  cdlemm10N  41120  dihvalcqpre  41237  dihopelvalcpre  41250  dihord5b  41261  dihglblem5apreN  41293  dihmeetlem16N  41324  dihmeetlem17N  41325  dvh3dim3N  41451  qirropth  42919  mzpcong  42984  jm2.26  43014  aomclem6  43071  limcleqr  45659  fourierdlem42  46164  submodneaddmod  47353  itsclc0b  48693