Theorem simpl3l 1226

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  tfisi  7680  omopth2  8377  ltmul1a  11754  xaddass  12912  xlemul2a  12952  swrdsbslen  14305  swrdspsleq  14306  dvdsadd2b  15943  pockthg  16535  psgnunilem4  19020  efgred  19269  ptbasin  22636  basqtop  22770  xrsmopn  23881  axpasch  27212  axcontlem4  27238  elwwlks2ons3im  28220  br4  33631  nosupbnd1lem3  33840  nosupbnd1lem4  33841  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  btwnintr  34248  btwnexch3  34249  btwnouttr2  34251  cgrxfr  34284  lineext  34305  btwnconn1lem13  34328  btwnconn1lem14  34329  btwnconn3  34332  brsegle  34337  brsegle2  34338  segleantisym  34344  outsideofeu  34360  lineunray  34376  lineelsb2  34377  cvrcmp  37224  atcvrj2b  37373  3dimlem3  37402  3dimlem3OLDN  37403  3dim3  37410  ps-1  37418  lplnnle2at  37482  2llnm3N  37510  lvolnle3at  37523  4atlem0a  37534  4atlem3  37537  4atlem3a  37538  lnatexN  37720  paddasslem8  37768  paddasslem9  37769  paddasslem10  37770  paddasslem12  37772  paddasslem13  37773  lhp2lt  37942  lhpexle2lem  37950  lhpexle3  37953  lhpmcvr3  37966  lhpat3  37987  4atex  38017  trlval2  38104  ltrnideq  38116  ltrnatlw  38124  trlnle  38127  trlval4  38129  cdlemd4  38142  cdlemd5  38143  cdleme16  38226  cdleme21  38278  cdleme21k  38279  cdleme27cl  38307  cdleme27N  38310  cdleme29ex  38315  cdleme43fsv1snlem  38361  cdleme40m  38408  cdleme46f2g2  38434  cdleme46f2g1  38435  trlord  38510  cdlemg8  38572  cdlemg15a  38596  cdlemg16z  38600  cdlemg18a  38619  cdlemg24  38629  cdlemg38  38656  cdlemg40  38658  trlcone  38669  cdlemj2  38763  tendoid0  38766  tendoconid  38770  cdlemk34  38851  cdlemk38  38856  cdlemkid4  38875  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk53  38898  tendospcanN  38964  cdlemm10N  39059  dihvalcqpre  39176  dihopelvalcpre  39189  dihord5b  39200  dihglblem5apreN  39232  dihmeetlem16N  39263  dihmeetlem17N  39264  dvh3dim3N  39390  qirropth  40646  mzpcong  40710  jm2.26  40740  aomclem6  40800  limcleqr  43075  fourierdlem42  43580  itsclc0b  46006