Theorem simpl3l 1225

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  tfisi  7869  omopth2  8611  ltmul1a  12101  xaddass  13268  xlemul2a  13308  swrdsbslen  14654  swrdspsleq  14655  dvdsadd2b  16290  pockthg  16882  psgnunilem4  19459  efgred  19710  ptbasin  23501  basqtop  23635  xrsmopn  24748  nosupbnd1lem3  27663  nosupbnd1lem4  27664  noinfbnd1lem3  27678  noinfbnd1lem4  27679  noinfbnd1lem5  27680  precsexlem8  28132  axpasch  28772  axcontlem4  28798  elwwlks2ons3im  29785  mhmimasplusg  32779  br4  35385  btwnintr  35648  btwnexch3  35649  btwnouttr2  35651  cgrxfr  35684  lineext  35705  btwnconn1lem13  35728  btwnconn1lem14  35729  btwnconn3  35732  brsegle  35737  brsegle2  35738  segleantisym  35744  outsideofeu  35760  lineunray  35776  lineelsb2  35777  cvrcmp  38787  atcvrj2b  38937  3dimlem3  38966  3dimlem3OLDN  38967  3dim3  38974  ps-1  38982  lplnnle2at  39046  2llnm3N  39074  lvolnle3at  39087  4atlem0a  39098  4atlem3  39101  4atlem3a  39102  lnatexN  39284  paddasslem8  39332  paddasslem9  39333  paddasslem10  39334  paddasslem12  39336  paddasslem13  39337  lhp2lt  39506  lhpexle2lem  39514  lhpexle3  39517  lhpmcvr3  39530  lhpat3  39551  4atex  39581  trlval2  39668  ltrnideq  39680  ltrnatlw  39688  trlnle  39691  trlval4  39693  cdlemd4  39706  cdlemd5  39707  cdleme16  39790  cdleme21  39842  cdleme21k  39843  cdleme27cl  39871  cdleme27N  39874  cdleme29ex  39879  cdleme43fsv1snlem  39925  cdleme40m  39972  cdleme46f2g2  39998  cdleme46f2g1  39999  trlord  40074  cdlemg8  40136  cdlemg15a  40160  cdlemg16z  40164  cdlemg18a  40183  cdlemg24  40193  cdlemg38  40220  cdlemg40  40222  trlcone  40233  cdlemj2  40327  tendoid0  40330  tendoconid  40334  cdlemk34  40415  cdlemk38  40420  cdlemkid4  40439  cdlemk35s-id  40443  cdlemk39s-id  40445  cdlemk53  40462  tendospcanN  40528  cdlemm10N  40623  dihvalcqpre  40740  dihopelvalcpre  40753  dihord5b  40764  dihglblem5apreN  40796  dihmeetlem16N  40827  dihmeetlem17N  40828  dvh3dim3N  40954  qirropth  42359  mzpcong  42424  jm2.26  42454  aomclem6  42514  limcleqr  45061  fourierdlem42  45566  itsclc0b  47923

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »