Theorem simpl3l 1247

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfisi  7870  omopth2  8593  ltmul1a  12167  xaddass  13380  xlemul2a  13420  swrdsbslen  14815  swrdspsleq  14816  dvdsadd2b  16477  pockthg  17085  psgnunilem4  19712  efgred  19963  ptbasin  23897  basqtop  24031  xrsmopn  25133  nosupbnd1lem3  28068  nosupbnd1lem4  28069  noinfbnd1lem3  28083  noinfbnd1lem4  28084  noinfbnd1lem5  28085  precsexlem8  28601  bdayfinbndlem1  28854  axpasch  29520  axcontlem4  29546  elwwlks2ons3im  30544  mhmimasplusg  33641  br4  36598  btwnintr  36859  btwnexch3  36860  btwnouttr2  36862  cgrxfr  36895  lineext  36916  btwnconn1lem13  36939  btwnconn1lem14  36940  btwnconn3  36943  brsegle  36948  brsegle2  36949  segleantisym  36955  outsideofeu  36971  lineunray  36987  lineelsb2  36988  cvrcmp  40416  atcvrj2b  40565  3dimlem3  40594  3dimlem3OLDN  40595  3dim3  40602  ps-1  40610  lplnnle2at  40674  2llnm3N  40702  lvolnle3at  40715  4atlem0a  40726  4atlem3  40729  4atlem3a  40730  lnatexN  40912  paddasslem8  40960  paddasslem9  40961  paddasslem10  40962  paddasslem12  40964  paddasslem13  40965  lhp2lt  41134  lhpexle2lem  41142  lhpexle3  41145  lhpmcvr3  41158  lhpat3  41179  4atex  41209  trlval2  41296  ltrnideq  41308  ltrnatlw  41316  trlnle  41319  trlval4  41321  cdlemd4  41334  cdlemd5  41335  cdleme16  41418  cdleme21  41470  cdleme21k  41471  cdleme27cl  41499  cdleme27N  41502  cdleme29ex  41507  cdleme43fsv1snlem  41553  cdleme40m  41600  cdleme46f2g2  41626  cdleme46f2g1  41627  trlord  41702  cdlemg8  41764  cdlemg15a  41788  cdlemg16z  41792  cdlemg18a  41811  cdlemg24  41821  cdlemg38  41848  cdlemg40  41850  trlcone  41861  cdlemj2  41955  tendoid0  41958  tendoconid  41962  cdlemk34  42043  cdlemk38  42048  cdlemkid4  42067  cdlemk35s-id  42071  cdlemk39s-id  42073  cdlemk53  42090  tendospcanN  42156  cdlemm10N  42251  dihvalcqpre  42368  dihopelvalcpre  42381  dihord5b  42392  dihglblem5apreN  42424  dihmeetlem16N  42455  dihmeetlem17N  42456  dvh3dim3N  42582  qirropth  43991  mzpcong  44055  jm2.26  44085  aomclem6  44137  limcleqr  46730  fourierdlem42  47235  submodneaddmod  48503  itsclc0b  49960