Theorem simp1 986

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)

Proof of Theorem simp1

Step	Hyp	Ref	Expression
1		3simpa 983	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simpld 111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  simpl1  989  simpr1  992  simp1i  995  simp1d  998  simp11  1016  simp21  1019  simp31  1022  syld3an3  1272  3ianorr  1298  stoic4a  1419  stoic4b  1420  rsp2e  2515  issod  4291  elirr  4512  sotri2  4995  sotri3  4996  funtpg  5233  funimaexglem  5265  feq123  5323  ftpg  5663  fsnunf  5679  foco2  5716  fcofo  5746  f1oiso2  5789  riotass  5819  ovmpox  5961  ovmpoga  5962  caovimo  6026  ofeq  6046  ofrval  6054  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  frecsuclem  6365  frecrdg  6367  mapxpen  6805  diffifi  6851  unsnfidcex  6876  unsnfidcel  6877  unfidisj  6878  undifdc  6880  ssfidc  6891  iunfidisj  6902  sbthlemi9  6921  elfir  6929  djuassen  7164  mulcanenq  7317  ltanqg  7332  addnnnq0  7381  distrlem4prl  7516  distrlem4pru  7517  distrprg  7520  aptipr  7573  addsrpr  7677  mulsrpr  7678  mulasssrg  7690  ltpsrprg  7735  axmulass  7805  axpre-ltadd  7818  mul31  8020  addsubass  8099  subcan2  8114  subsub2  8117  subsub4  8122  npncan3  8127  pnpcan  8128  pnncan  8130  subcan  8144  subdi  8274  ltadd1  8318  leadd1  8319  leadd2  8320  ltsubadd  8321  lesubadd  8323  ltaddsub  8325  leaddsub  8327  lesub1  8345  lesub2  8346  ltsub1  8347  ltsub2  8348  ltaddsublt  8460  gt0add  8462  apreap  8476  lemul1  8482  reapmul1lem  8483  reapmul1  8484  reapadd1  8485  remulext1  8488  remulext2  8489  apadd2  8498  mulext2  8502  mulap0r  8504  leltap  8514  ltap  8522  apsub1  8531  recexaplem2  8540  mulcanap  8553  mulcanap2  8554  divvalap  8561  divcanap2  8567  diveqap0  8569  divrecap  8575  divrecap2  8576  divdirap  8584  divcanap3  8585  div11ap  8587  muldivdirap  8594  divcanap5  8601  redivclap  8618  div2negap  8622  apmul1  8675  apmul2  8676  div2subap  8724  ltdiv1  8754  ltmuldiv  8760  lemuldiv  8767  lt2msq1  8771  ltdiv23  8778  lediv23  8779  squeeze0  8790  difgtsumgt  9251  gtndiv  9277  eluz2  9463  eluzsub  9486  peano2uz  9512  nn01to3  9546  divge1  9650  ledivge1le  9653  addlelt  9695  xaddass  9796  xleadd1  9802  xltadd1  9803  ixxssixx  9829  lbico1  9857  lbicc2  9911  icoshftf1o  9918  fzen  9968  fzrev3  10012  fzrevral2  10031  elfzo0  10107  elfzo0z  10109  fzosplitprm1  10159  qbtwnre  10182  flqwordi  10213  flqword2  10214  adddivflid  10217  flltdivnn0lt  10229  modqcl  10251  mulqmod0  10255  modqmulnn  10267  modqabs2  10283  addmodid  10297  modifeq2int  10311  modqeqmodmin  10319  seqeq2  10374  seqeq3  10375  exp3val  10447  expnegap0  10453  expgt1  10483  exprecap  10486  leexp2a  10498  expubnd  10502  sqdivap  10509  expnbnd  10567  bccmpl  10656  fihashss  10718  leisorel  10736  shftfibg  10748  mulreap  10792  abssubne0  11019  maxleast  11141  lemininf  11161  ltmininf  11162  xrmaxltsup  11185  xrmaxaddlem  11187  xrmaxadd  11188  xrmineqinf  11196  xrltmininf  11197  xrminltinf  11199  xrminadd  11202  climuni  11220  reccn2ap  11240  isumz  11316  fsumsplitsnun  11346  geoisum1c  11447  prod1dc  11513  efltim  11625  dvdscmulr  11746  dvdsmulcr  11747  summodnegmod  11748  modmulconst  11749  dvdsmultr2  11758  dvdsexp  11784  mulmoddvds  11786  modremain  11851  divgcdz  11889  gcdaddm  11902  dvdsgcdb  11931  gcdass  11933  mulgcd  11934  gcddiv  11937  rplpwr  11945  lcmdvdsb  11995  lcmass  11996  mulgcddvds  12005  qredeq  12007  qredeu  12008  rpmul  12009  divgcdcoprmex  12013  cncongr1  12014  rpexp  12062  rpexp12i  12064  odzcllem  12151  odzdvds  12154  odzphi  12155  pythagtriplem15  12187  pcpremul  12202  pcdiv  12211  pcqmul  12212  pcqdiv  12216  dvdsprmpweq  12243  sumhashdc  12254  pcfaclem  12256  qexpz  12259  ctinf  12300  setsvala  12362  ressid2  12390  ressval2  12391  rngbaseg  12447  2basgeng  12623  clsss  12659  ntrss  12660  ntrin  12665  neiss  12691  restco  12715  restabs  12716  lmconst  12757  psmetsym  12870  psmetge0  12872  xmetge0  12906  xmetsym  12909  xmetresbl  12981  mopni3  13025  bdxmet  13042  bdmopn  13045  txmetcnp  13059  dvfvalap  13191  dvid  13203  dvcnp2cntop  13204  ptolemy  13286  rpcxpadd  13367  rpmulcxp  13371  rpdivcxp  13373  cxpmul  13374  rpcxple2  13379  rpcxplt2  13380  cxpcom  13398  rplogbval  13404  rplogbcl  13405  rprelogbmulexp  13415  relogbexpap  13417  logbleb  13420  logblt  13421  rplogbcxp  13422  rpcxplogb  13423