Theorem simpl3l 1224

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  tfisi  7567  omopth2  8204  ltmul1a  11483  xaddass  12636  xlemul2a  12676  swrdsbslen  14020  swrdspsleq  14021  dvdsadd2b  15650  pockthg  16236  psgnunilem4  18619  efgred  18868  ptbasin  22179  basqtop  22313  xrsmopn  23414  axpasch  26721  axcontlem4  26747  elwwlks2ons3im  27727  br4  32989  nosupbnd1lem3  33205  nosupbnd1lem4  33206  btwnintr  33475  btwnexch3  33476  btwnouttr2  33478  cgrxfr  33511  lineext  33532  btwnconn1lem13  33555  btwnconn1lem14  33556  btwnconn3  33559  brsegle  33564  brsegle2  33565  segleantisym  33571  outsideofeu  33587  lineunray  33603  lineelsb2  33604  cvrcmp  36413  atcvrj2b  36562  3dimlem3  36591  3dimlem3OLDN  36592  3dim3  36599  ps-1  36607  lplnnle2at  36671  2llnm3N  36699  lvolnle3at  36712  4atlem0a  36723  4atlem3  36726  4atlem3a  36727  lnatexN  36909  paddasslem8  36957  paddasslem9  36958  paddasslem10  36959  paddasslem12  36961  paddasslem13  36962  lhp2lt  37131  lhpexle2lem  37139  lhpexle3  37142  lhpmcvr3  37155  lhpat3  37176  4atex  37206  trlval2  37293  ltrnideq  37305  ltrnatlw  37313  trlnle  37316  trlval4  37318  cdlemd4  37331  cdlemd5  37332  cdleme16  37415  cdleme21  37467  cdleme21k  37468  cdleme27cl  37496  cdleme27N  37499  cdleme29ex  37504  cdleme43fsv1snlem  37550  cdleme40m  37597  cdleme46f2g2  37623  cdleme46f2g1  37624  trlord  37699  cdlemg8  37761  cdlemg15a  37785  cdlemg16z  37789  cdlemg18a  37808  cdlemg24  37818  cdlemg38  37845  cdlemg40  37847  trlcone  37858  cdlemj2  37952  tendoid0  37955  tendoconid  37959  cdlemk34  38040  cdlemk38  38045  cdlemkid4  38064  cdlemk35s-id  38068  cdlemk39s-id  38070  cdlemk53  38087  tendospcanN  38153  cdlemm10N  38248  dihvalcqpre  38365  dihopelvalcpre  38378  dihord5b  38389  dihglblem5apreN  38421  dihmeetlem16N  38452  dihmeetlem17N  38453  dvh3dim3N  38579  qirropth  39498  mzpcong  39562  jm2.26  39592  aomclem6  39652  limcleqr  41918  fourierdlem42  42428  itsclc0b  44753