Theorem simpl3l 1229

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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl3 1188	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfisi  7798  omopth2  8508  ltmul1a  11980  xaddass  13158  xlemul2a  13198  swrdsbslen  14582  swrdspsleq  14583  dvdsadd2b  16227  pockthg  16828  psgnunilem4  19419  efgred  19670  ptbasin  23502  basqtop  23636  xrsmopn  24738  nosupbnd1lem3  27659  nosupbnd1lem4  27660  noinfbnd1lem3  27674  noinfbnd1lem4  27675  noinfbnd1lem5  27676  precsexlem8  28162  axpasch  28930  axcontlem4  28956  elwwlks2ons3im  29943  mhmimasplusg  33030  br4  35813  btwnintr  36074  btwnexch3  36075  btwnouttr2  36077  cgrxfr  36110  lineext  36131  btwnconn1lem13  36154  btwnconn1lem14  36155  btwnconn3  36158  brsegle  36163  brsegle2  36164  segleantisym  36170  outsideofeu  36186  lineunray  36202  lineelsb2  36203  cvrcmp  39392  atcvrj2b  39541  3dimlem3  39570  3dimlem3OLDN  39571  3dim3  39578  ps-1  39586  lplnnle2at  39650  2llnm3N  39678  lvolnle3at  39691  4atlem0a  39702  4atlem3  39705  4atlem3a  39706  lnatexN  39888  paddasslem8  39936  paddasslem9  39937  paddasslem10  39938  paddasslem12  39940  paddasslem13  39941  lhp2lt  40110  lhpexle2lem  40118  lhpexle3  40121  lhpmcvr3  40134  lhpat3  40155  4atex  40185  trlval2  40272  ltrnideq  40284  ltrnatlw  40292  trlnle  40295  trlval4  40297  cdlemd4  40310  cdlemd5  40311  cdleme16  40394  cdleme21  40446  cdleme21k  40447  cdleme27cl  40475  cdleme27N  40478  cdleme29ex  40483  cdleme43fsv1snlem  40529  cdleme40m  40576  cdleme46f2g2  40602  cdleme46f2g1  40603  trlord  40678  cdlemg8  40740  cdlemg15a  40764  cdlemg16z  40768  cdlemg18a  40787  cdlemg24  40797  cdlemg38  40824  cdlemg40  40826  trlcone  40837  cdlemj2  40931  tendoid0  40934  tendoconid  40938  cdlemk34  41019  cdlemk38  41024  cdlemkid4  41043  cdlemk35s-id  41047  cdlemk39s-id  41049  cdlemk53  41066  tendospcanN  41132  cdlemm10N  41227  dihvalcqpre  41344  dihopelvalcpre  41357  dihord5b  41368  dihglblem5apreN  41400  dihmeetlem16N  41431  dihmeetlem17N  41432  dvh3dim3N  41558  qirropth  43015  mzpcong  43079  jm2.26  43109  aomclem6  43166  limcleqr  45756  fourierdlem42  46261  submodneaddmod  47465  itsclc0b  48887