Theorem simpl3l 1230

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 1189	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  7803  omopth2  8513  ltmul1a  11994  xaddass  13168  xlemul2a  13208  swrdsbslen  14592  swrdspsleq  14593  dvdsadd2b  16237  pockthg  16838  psgnunilem4  19430  efgred  19681  ptbasin  23525  basqtop  23659  xrsmopn  24761  nosupbnd1lem3  27682  nosupbnd1lem4  27683  noinfbnd1lem3  27697  noinfbnd1lem4  27698  noinfbnd1lem5  27699  precsexlem8  28195  bdayfinbndlem1  28446  axpasch  28997  axcontlem4  29023  elwwlks2ons3im  30010  mhmimasplusg  33101  br4  35933  btwnintr  36194  btwnexch3  36195  btwnouttr2  36197  cgrxfr  36230  lineext  36251  btwnconn1lem13  36274  btwnconn1lem14  36275  btwnconn3  36278  brsegle  36283  brsegle2  36284  segleantisym  36290  outsideofeu  36306  lineunray  36322  lineelsb2  36323  cvrcmp  39580  atcvrj2b  39729  3dimlem3  39758  3dimlem3OLDN  39759  3dim3  39766  ps-1  39774  lplnnle2at  39838  2llnm3N  39866  lvolnle3at  39879  4atlem0a  39890  4atlem3  39893  4atlem3a  39894  lnatexN  40076  paddasslem8  40124  paddasslem9  40125  paddasslem10  40126  paddasslem12  40128  paddasslem13  40129  lhp2lt  40298  lhpexle2lem  40306  lhpexle3  40309  lhpmcvr3  40322  lhpat3  40343  4atex  40373  trlval2  40460  ltrnideq  40472  ltrnatlw  40480  trlnle  40483  trlval4  40485  cdlemd4  40498  cdlemd5  40499  cdleme16  40582  cdleme21  40634  cdleme21k  40635  cdleme27cl  40663  cdleme27N  40666  cdleme29ex  40671  cdleme43fsv1snlem  40717  cdleme40m  40764  cdleme46f2g2  40790  cdleme46f2g1  40791  trlord  40866  cdlemg8  40928  cdlemg15a  40952  cdlemg16z  40956  cdlemg18a  40975  cdlemg24  40985  cdlemg38  41012  cdlemg40  41014  trlcone  41025  cdlemj2  41119  tendoid0  41122  tendoconid  41126  cdlemk34  41207  cdlemk38  41212  cdlemkid4  41231  cdlemk35s-id  41235  cdlemk39s-id  41237  cdlemk53  41254  tendospcanN  41320  cdlemm10N  41415  dihvalcqpre  41532  dihopelvalcpre  41545  dihord5b  41556  dihglblem5apreN  41588  dihmeetlem16N  41619  dihmeetlem17N  41620  dvh3dim3N  41746  qirropth  43186  mzpcong  43250  jm2.26  43280  aomclem6  43337  limcleqr  45924  fourierdlem42  46429  submodneaddmod  47633  itsclc0b  49054