Theorem simpl3l 1227

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  tfisi  7714  omopth2  8424  ltmul1a  11833  xaddass  12992  xlemul2a  13032  swrdsbslen  14386  swrdspsleq  14387  dvdsadd2b  16024  pockthg  16616  psgnunilem4  19114  efgred  19363  ptbasin  22737  basqtop  22871  xrsmopn  23984  axpasch  27318  axcontlem4  27344  elwwlks2ons3im  28328  br4  33734  nosupbnd1lem3  33922  nosupbnd1lem4  33923  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  btwnintr  34330  btwnexch3  34331  btwnouttr2  34333  cgrxfr  34366  lineext  34387  btwnconn1lem13  34410  btwnconn1lem14  34411  btwnconn3  34414  brsegle  34419  brsegle2  34420  segleantisym  34426  outsideofeu  34442  lineunray  34458  lineelsb2  34459  cvrcmp  37304  atcvrj2b  37453  3dimlem3  37482  3dimlem3OLDN  37483  3dim3  37490  ps-1  37498  lplnnle2at  37562  2llnm3N  37590  lvolnle3at  37603  4atlem0a  37614  4atlem3  37617  4atlem3a  37618  lnatexN  37800  paddasslem8  37848  paddasslem9  37849  paddasslem10  37850  paddasslem12  37852  paddasslem13  37853  lhp2lt  38022  lhpexle2lem  38030  lhpexle3  38033  lhpmcvr3  38046  lhpat3  38067  4atex  38097  trlval2  38184  ltrnideq  38196  ltrnatlw  38204  trlnle  38207  trlval4  38209  cdlemd4  38222  cdlemd5  38223  cdleme16  38306  cdleme21  38358  cdleme21k  38359  cdleme27cl  38387  cdleme27N  38390  cdleme29ex  38395  cdleme43fsv1snlem  38441  cdleme40m  38488  cdleme46f2g2  38514  cdleme46f2g1  38515  trlord  38590  cdlemg8  38652  cdlemg15a  38676  cdlemg16z  38680  cdlemg18a  38699  cdlemg24  38709  cdlemg38  38736  cdlemg40  38738  trlcone  38749  cdlemj2  38843  tendoid0  38846  tendoconid  38850  cdlemk34  38931  cdlemk38  38936  cdlemkid4  38955  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk53  38978  tendospcanN  39044  cdlemm10N  39139  dihvalcqpre  39256  dihopelvalcpre  39269  dihord5b  39280  dihglblem5apreN  39312  dihmeetlem16N  39343  dihmeetlem17N  39344  dvh3dim3N  39470  qirropth  40737  mzpcong  40801  jm2.26  40831  aomclem6  40891  limcleqr  43192  fourierdlem42  43697  itsclc0b  46129