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  7572  omopth2  8209  ltmul1a  11488  xaddass  12641  xlemul2a  12681  swrdsbslen  14025  swrdspsleq  14026  dvdsadd2b  15655  pockthg  16241  psgnunilem4  18624  efgred  18873  ptbasin  22184  basqtop  22318  xrsmopn  23419  axpasch  26726  axcontlem4  26752  elwwlks2ons3im  27732  br4  32994  nosupbnd1lem3  33210  nosupbnd1lem4  33211  btwnintr  33480  btwnexch3  33481  btwnouttr2  33483  cgrxfr  33516  lineext  33537  btwnconn1lem13  33560  btwnconn1lem14  33561  btwnconn3  33564  brsegle  33569  brsegle2  33570  segleantisym  33576  outsideofeu  33592  lineunray  33608  lineelsb2  33609  cvrcmp  36418  atcvrj2b  36567  3dimlem3  36596  3dimlem3OLDN  36597  3dim3  36604  ps-1  36612  lplnnle2at  36676  2llnm3N  36704  lvolnle3at  36717  4atlem0a  36728  4atlem3  36731  4atlem3a  36732  lnatexN  36914  paddasslem8  36962  paddasslem9  36963  paddasslem10  36964  paddasslem12  36966  paddasslem13  36967  lhp2lt  37136  lhpexle2lem  37144  lhpexle3  37147  lhpmcvr3  37160  lhpat3  37181  4atex  37211  trlval2  37298  ltrnideq  37310  ltrnatlw  37318  trlnle  37321  trlval4  37323  cdlemd4  37336  cdlemd5  37337  cdleme16  37420  cdleme21  37472  cdleme21k  37473  cdleme27cl  37501  cdleme27N  37504  cdleme29ex  37509  cdleme43fsv1snlem  37555  cdleme40m  37602  cdleme46f2g2  37628  cdleme46f2g1  37629  trlord  37704  cdlemg8  37766  cdlemg15a  37790  cdlemg16z  37794  cdlemg18a  37813  cdlemg24  37823  cdlemg38  37850  cdlemg40  37852  trlcone  37863  cdlemj2  37957  tendoid0  37960  tendoconid  37964  cdlemk34  38045  cdlemk38  38050  cdlemkid4  38069  cdlemk35s-id  38073  cdlemk39s-id  38075  cdlemk53  38092  tendospcanN  38158  cdlemm10N  38253  dihvalcqpre  38370  dihopelvalcpre  38383  dihord5b  38394  dihglblem5apreN  38426  dihmeetlem16N  38457  dihmeetlem17N  38458  dvh3dim3N  38584  qirropth  39503  mzpcong  39567  jm2.26  39597  aomclem6  39657  limcleqr  41923  fourierdlem42  42433  itsclc0b  44758