Theorem simp1 941

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 938	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simpld 110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  simpl1  944  simpr1  947  simp1i  950  simp1d  953  simp11  971  simp21  974  simp31  977  syld3an3  1217  3ianorr  1243  stoic4a  1364  stoic4b  1365  rsp2e  2422  issod  4120  elirr  4330  sotri2  4796  sotri3  4797  funtpg  5030  funimaexglem  5062  feq123  5118  ftpg  5444  fsnunf  5459  foco2  5494  fcofo  5524  f1oiso2  5567  riotass  5596  ovmpt2x  5730  ovmpt2ga  5731  caovimo  5795  ofeq  5815  ofrval  5823  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  frecsuclem  6125  frecrdg  6127  mapxpen  6516  diffifi  6562  unsnfidcex  6582  unsnfidcel  6583  unfidisj  6584  undifdc  6586  ssfidc  6594  sbthlemi9  6618  mulcanenq  6888  ltanqg  6903  addnnnq0  6952  distrlem4prl  7087  distrlem4pru  7088  distrprg  7091  aptipr  7144  addsrpr  7235  mulsrpr  7236  mulasssrg  7248  axmulass  7352  axpre-ltadd  7365  mul31  7557  addsubass  7636  subcan2  7651  subsub2  7654  subsub4  7659  npncan3  7664  pnpcan  7665  pnncan  7667  subcan  7681  subdi  7807  ltadd1  7851  leadd1  7852  leadd2  7853  ltsubadd  7854  lesubadd  7856  ltaddsub  7858  leaddsub  7860  lesub1  7878  lesub2  7879  ltsub1  7880  ltsub2  7881  ltaddsublt  7989  gt0add  7991  apreap  8005  lemul1  8011  reapmul1lem  8012  reapmul1  8013  reapadd1  8014  remulext1  8017  remulext2  8018  apadd2  8027  mulext2  8031  mulap0r  8033  leltap  8042  ltap  8049  recexaplem2  8060  mulcanap  8073  mulcanap2  8074  divvalap  8080  divcanap2  8086  diveqap0  8088  divrecap  8094  divrecap2  8095  divdirap  8103  divcanap3  8104  div11ap  8106  muldivdirap  8113  divcanap5  8120  redivclap  8137  div2negap  8141  apmul1  8194  ltdiv1  8264  ltmuldiv  8270  lemuldiv  8277  lt2msq1  8281  ltdiv23  8288  lediv23  8289  squeeze0  8300  gtndiv  8774  eluz2  8957  eluzsub  8980  peano2uz  9003  nn01to3  9034  divge1  9132  ledivge1le  9135  addlelt  9171  ixxssixx  9252  lbico1  9280  lbicc2  9333  icoshftf1o  9340  fzen  9389  fzrev3  9431  fzrevral2  9450  elfzo0  9521  elfzo0z  9523  fzosplitprm1  9573  qbtwnre  9596  flqwordi  9623  flqword2  9624  adddivflid  9627  flltdivnn0lt  9639  modqcl  9661  mulqmod0  9665  modqmulnn  9677  modqabs2  9693  addmodid  9707  modifeq2int  9721  modqeqmodmin  9729  iseqeq2  9783  iseqeq3  9784  expnegap0  9862  expgt1  9892  exprecap  9895  leexp2a  9907  expubnd  9911  sqdivap  9918  expnbnd  9974  bccmpl  10059  fihashss  10121  leisorel  10139  shftfibg  10151  mulreap  10194  abssubne0  10420  maxleast  10542  lemininf  10559  ltmininf  10560  climuni  10576  isumz  10669  dvdscmulr  10707  dvdsmulcr  10708  summodnegmod  10709  modmulconst  10710  dvdsmultr2  10718  dvdsexp  10744  mulmoddvds  10746  modremain  10811  divgcdz  10845  gcdaddm  10857  dvdsgcdb  10884  gcdass  10886  mulgcd  10887  gcddiv  10890  rplpwr  10898  lcmdvdsb  10948  lcmass  10949  mulgcddvds  10958  qredeq  10960  qredeu  10961  rpmul  10962  divgcdcoprmex  10966  cncongr1  10967  rpexp  11014  rpexp12i  11016