Theorem simpl3l 1228

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 1187	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

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

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 1089

This theorem is referenced by:  tfisi  7896  omopth2  8640  ltmul1a  12143  xaddass  13311  xlemul2a  13351  swrdsbslen  14712  swrdspsleq  14713  dvdsadd2b  16354  pockthg  16953  psgnunilem4  19539  efgred  19790  ptbasin  23606  basqtop  23740  xrsmopn  24853  nosupbnd1lem3  27773  nosupbnd1lem4  27774  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  precsexlem8  28256  axpasch  28974  axcontlem4  29000  elwwlks2ons3im  29987  mhmimasplusg  33024  br4  35720  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  cgrxfr  36019  lineext  36040  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  brsegle  36072  brsegle2  36073  segleantisym  36079  outsideofeu  36095  lineunray  36111  lineelsb2  36112  cvrcmp  39239  atcvrj2b  39389  3dimlem3  39418  3dimlem3OLDN  39419  3dim3  39426  ps-1  39434  lplnnle2at  39498  2llnm3N  39526  lvolnle3at  39539  4atlem0a  39550  4atlem3  39553  4atlem3a  39554  lnatexN  39736  paddasslem8  39784  paddasslem9  39785  paddasslem10  39786  paddasslem12  39788  paddasslem13  39789  lhp2lt  39958  lhpexle2lem  39966  lhpexle3  39969  lhpmcvr3  39982  lhpat3  40003  4atex  40033  trlval2  40120  ltrnideq  40132  ltrnatlw  40140  trlnle  40143  trlval4  40145  cdlemd4  40158  cdlemd5  40159  cdleme16  40242  cdleme21  40294  cdleme21k  40295  cdleme27cl  40323  cdleme27N  40326  cdleme29ex  40331  cdleme43fsv1snlem  40377  cdleme40m  40424  cdleme46f2g2  40450  cdleme46f2g1  40451  trlord  40526  cdlemg8  40588  cdlemg15a  40612  cdlemg16z  40616  cdlemg18a  40635  cdlemg24  40645  cdlemg38  40672  cdlemg40  40674  trlcone  40685  cdlemj2  40779  tendoid0  40782  tendoconid  40786  cdlemk34  40867  cdlemk38  40872  cdlemkid4  40891  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk53  40914  tendospcanN  40980  cdlemm10N  41075  dihvalcqpre  41192  dihopelvalcpre  41205  dihord5b  41216  dihglblem5apreN  41248  dihmeetlem16N  41279  dihmeetlem17N  41280  dvh3dim3N  41406  qirropth  42864  mzpcong  42929  jm2.26  42959  aomclem6  43016  limcleqr  45565  fourierdlem42  46070  itsclc0b  48506