Theorem simpl3l 1238

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

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

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 1097

This theorem is referenced by:  tfisi  7828  omopth2  8541  ltmul1a  12030  xaddass  13242  xlemul2a  13282  swrdsbslen  14668  swrdspsleq  14669  dvdsadd2b  16316  pockthg  16918  psgnunilem4  19513  efgred  19764  ptbasin  23610  basqtop  23744  xrsmopn  24846  nosupbnd1lem3  27744  nosupbnd1lem4  27745  noinfbnd1lem3  27759  noinfbnd1lem4  27760  noinfbnd1lem5  27761  precsexlem8  28277  bdayfinbndlem1  28530  axpasch  29081  axcontlem4  29107  elwwlks2ons3im  30093  mhmimasplusg  33170  br4  36056  btwnintr  36317  btwnexch3  36318  btwnouttr2  36320  cgrxfr  36353  lineext  36374  btwnconn1lem13  36397  btwnconn1lem14  36398  btwnconn3  36401  brsegle  36406  brsegle2  36407  segleantisym  36413  outsideofeu  36429  lineunray  36445  lineelsb2  36446  cvrcmp  39855  atcvrj2b  40004  3dimlem3  40033  3dimlem3OLDN  40034  3dim3  40041  ps-1  40049  lplnnle2at  40113  2llnm3N  40141  lvolnle3at  40154  4atlem0a  40165  4atlem3  40168  4atlem3a  40169  lnatexN  40351  paddasslem8  40399  paddasslem9  40400  paddasslem10  40401  paddasslem12  40403  paddasslem13  40404  lhp2lt  40573  lhpexle2lem  40581  lhpexle3  40584  lhpmcvr3  40597  lhpat3  40618  4atex  40648  trlval2  40735  ltrnideq  40747  ltrnatlw  40755  trlnle  40758  trlval4  40760  cdlemd4  40773  cdlemd5  40774  cdleme16  40857  cdleme21  40909  cdleme21k  40910  cdleme27cl  40938  cdleme27N  40941  cdleme29ex  40946  cdleme43fsv1snlem  40992  cdleme40m  41039  cdleme46f2g2  41065  cdleme46f2g1  41066  trlord  41141  cdlemg8  41203  cdlemg15a  41227  cdlemg16z  41231  cdlemg18a  41250  cdlemg24  41260  cdlemg38  41287  cdlemg40  41289  trlcone  41300  cdlemj2  41394  tendoid0  41397  tendoconid  41401  cdlemk34  41482  cdlemk38  41487  cdlemkid4  41506  cdlemk35s-id  41510  cdlemk39s-id  41512  cdlemk53  41529  tendospcanN  41595  cdlemm10N  41690  dihvalcqpre  41807  dihopelvalcpre  41820  dihord5b  41831  dihglblem5apreN  41863  dihmeetlem16N  41894  dihmeetlem17N  41895  dvh3dim3N  42021  qirropth  43433  mzpcong  43497  jm2.26  43527  aomclem6  43584  limcleqr  46166  fourierdlem42  46671  submodneaddmod  47899  itsclc0b  49342