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  7799  omopth2  8509  ltmul1a  11991  xaddass  13169  xlemul2a  13209  swrdsbslen  14589  swrdspsleq  14590  dvdsadd2b  16235  pockthg  16836  psgnunilem4  19394  efgred  19645  ptbasin  23480  basqtop  23614  xrsmopn  24717  nosupbnd1lem3  27638  nosupbnd1lem4  27639  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  precsexlem8  28139  axpasch  28904  axcontlem4  28930  elwwlks2ons3im  29917  mhmimasplusg  33005  br4  35730  btwnintr  35992  btwnexch3  35993  btwnouttr2  35995  cgrxfr  36028  lineext  36049  btwnconn1lem13  36072  btwnconn1lem14  36073  btwnconn3  36076  brsegle  36081  brsegle2  36082  segleantisym  36088  outsideofeu  36104  lineunray  36120  lineelsb2  36121  cvrcmp  39261  atcvrj2b  39411  3dimlem3  39440  3dimlem3OLDN  39441  3dim3  39448  ps-1  39456  lplnnle2at  39520  2llnm3N  39548  lvolnle3at  39561  4atlem0a  39572  4atlem3  39575  4atlem3a  39576  lnatexN  39758  paddasslem8  39806  paddasslem9  39807  paddasslem10  39808  paddasslem12  39810  paddasslem13  39811  lhp2lt  39980  lhpexle2lem  39988  lhpexle3  39991  lhpmcvr3  40004  lhpat3  40025  4atex  40055  trlval2  40142  ltrnideq  40154  ltrnatlw  40162  trlnle  40165  trlval4  40167  cdlemd4  40180  cdlemd5  40181  cdleme16  40264  cdleme21  40316  cdleme21k  40317  cdleme27cl  40345  cdleme27N  40348  cdleme29ex  40353  cdleme43fsv1snlem  40399  cdleme40m  40446  cdleme46f2g2  40472  cdleme46f2g1  40473  trlord  40548  cdlemg8  40610  cdlemg15a  40634  cdlemg16z  40638  cdlemg18a  40657  cdlemg24  40667  cdlemg38  40694  cdlemg40  40696  trlcone  40707  cdlemj2  40801  tendoid0  40804  tendoconid  40808  cdlemk34  40889  cdlemk38  40894  cdlemkid4  40913  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk53  40936  tendospcanN  41002  cdlemm10N  41097  dihvalcqpre  41214  dihopelvalcpre  41227  dihord5b  41238  dihglblem5apreN  41270  dihmeetlem16N  41301  dihmeetlem17N  41302  dvh3dim3N  41428  qirropth  42881  mzpcong  42945  jm2.26  42975  aomclem6  43032  limcleqr  45626  fourierdlem42  46131  submodneaddmod  47336  itsclc0b  48745