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 395   ∧ 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 396  df-3an 1088

This theorem is referenced by:  tfisi  7852  omopth2  8590  ltmul1a  12070  xaddass  13235  xlemul2a  13275  swrdsbslen  14621  swrdspsleq  14622  dvdsadd2b  16256  pockthg  16846  psgnunilem4  19413  efgred  19664  ptbasin  23401  basqtop  23535  xrsmopn  24648  nosupbnd1lem3  27557  nosupbnd1lem4  27558  noinfbnd1lem3  27572  noinfbnd1lem4  27573  noinfbnd1lem5  27574  precsexlem8  28026  axpasch  28633  axcontlem4  28659  elwwlks2ons3im  29642  mhmimasplusg  32633  br4  35199  btwnintr  35462  btwnexch3  35463  btwnouttr2  35465  cgrxfr  35498  lineext  35519  btwnconn1lem13  35542  btwnconn1lem14  35543  btwnconn3  35546  brsegle  35551  brsegle2  35552  segleantisym  35558  outsideofeu  35574  lineunray  35590  lineelsb2  35591  cvrcmp  38619  atcvrj2b  38769  3dimlem3  38798  3dimlem3OLDN  38799  3dim3  38806  ps-1  38814  lplnnle2at  38878  2llnm3N  38906  lvolnle3at  38919  4atlem0a  38930  4atlem3  38933  4atlem3a  38934  lnatexN  39116  paddasslem8  39164  paddasslem9  39165  paddasslem10  39166  paddasslem12  39168  paddasslem13  39169  lhp2lt  39338  lhpexle2lem  39346  lhpexle3  39349  lhpmcvr3  39362  lhpat3  39383  4atex  39413  trlval2  39500  ltrnideq  39512  ltrnatlw  39520  trlnle  39523  trlval4  39525  cdlemd4  39538  cdlemd5  39539  cdleme16  39622  cdleme21  39674  cdleme21k  39675  cdleme27cl  39703  cdleme27N  39706  cdleme29ex  39711  cdleme43fsv1snlem  39757  cdleme40m  39804  cdleme46f2g2  39830  cdleme46f2g1  39831  trlord  39906  cdlemg8  39968  cdlemg15a  39992  cdlemg16z  39996  cdlemg18a  40015  cdlemg24  40025  cdlemg38  40052  cdlemg40  40054  trlcone  40065  cdlemj2  40159  tendoid0  40162  tendoconid  40166  cdlemk34  40247  cdlemk38  40252  cdlemkid4  40271  cdlemk35s-id  40275  cdlemk39s-id  40277  cdlemk53  40294  tendospcanN  40360  cdlemm10N  40455  dihvalcqpre  40572  dihopelvalcpre  40585  dihord5b  40596  dihglblem5apreN  40628  dihmeetlem16N  40659  dihmeetlem17N  40660  dvh3dim3N  40786  qirropth  42111  mzpcong  42176  jm2.26  42206  aomclem6  42266  limcleqr  44821  fourierdlem42  45326  itsclc0b  47622