Theorem simp1 992

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

Syntax hints:   → wi 4   ∧ w3a 973

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 975

This theorem is referenced by:  simpl1  995  simpr1  998  simp1i  1001  simp1d  1004  simp11  1022  simp21  1025  simp31  1028  syld3an3  1278  3ianorr  1304  stoic4a  1425  stoic4b  1426  rsp2e  2521  issod  4304  elirr  4525  sotri2  5008  sotri3  5009  funtpg  5249  funimaexglem  5281  feq123  5339  ftpg  5680  fsnunf  5696  foco2  5733  fcofo  5763  f1oiso2  5806  riotass  5836  ovmpox  5981  ovmpoga  5982  caovimo  6046  ofeq  6063  ofrval  6071  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  frecsuclem  6385  frecrdg  6387  mapxpen  6826  diffifi  6872  unsnfidcex  6897  unsnfidcel  6898  unfidisj  6899  undifdc  6901  ssfidc  6912  iunfidisj  6923  sbthlemi9  6942  elfir  6950  djuassen  7194  mulcanenq  7347  ltanqg  7362  addnnnq0  7411  distrlem4prl  7546  distrlem4pru  7547  distrprg  7550  aptipr  7603  addsrpr  7707  mulsrpr  7708  mulasssrg  7720  ltpsrprg  7765  axmulass  7835  axpre-ltadd  7848  mul31  8050  addsubass  8129  subcan2  8144  subsub2  8147  subsub4  8152  npncan3  8157  pnpcan  8158  pnncan  8160  subcan  8174  subdi  8304  ltadd1  8348  leadd1  8349  leadd2  8350  ltsubadd  8351  lesubadd  8353  ltaddsub  8355  leaddsub  8357  lesub1  8375  lesub2  8376  ltsub1  8377  ltsub2  8378  ltaddsublt  8490  gt0add  8492  apreap  8506  lemul1  8512  reapmul1lem  8513  reapmul1  8514  reapadd1  8515  remulext1  8518  remulext2  8519  apadd2  8528  mulext2  8532  mulap0r  8534  leltap  8544  ltap  8552  apsub1  8561  recexaplem2  8570  mulcanap  8583  mulcanap2  8584  divvalap  8591  divcanap2  8597  diveqap0  8599  divrecap  8605  divrecap2  8606  divdirap  8614  divcanap3  8615  div11ap  8617  muldivdirap  8624  divcanap5  8631  redivclap  8648  div2negap  8652  apmul1  8705  apmul2  8706  div2subap  8754  ltdiv1  8784  ltmuldiv  8790  lemuldiv  8797  lt2msq1  8801  ltdiv23  8808  lediv23  8809  squeeze0  8820  difgtsumgt  9281  gtndiv  9307  eluz2  9493  eluzsub  9516  peano2uz  9542  nn01to3  9576  divge1  9680  ledivge1le  9683  addlelt  9725  xaddass  9826  xleadd1  9832  xltadd1  9833  ixxssixx  9859  lbico1  9887  lbicc2  9941  icoshftf1o  9948  fzen  9999  fzrev3  10043  fzrevral2  10062  elfzo0  10138  elfzo0z  10140  fzosplitprm1  10190  qbtwnre  10213  flqwordi  10244  flqword2  10245  adddivflid  10248  flltdivnn0lt  10260  modqcl  10282  mulqmod0  10286  modqmulnn  10298  modqabs2  10314  addmodid  10328  modifeq2int  10342  modqeqmodmin  10350  seqeq2  10405  seqeq3  10406  exp3val  10478  expnegap0  10484  expgt1  10514  exprecap  10517  leexp2a  10529  expubnd  10533  sqdivap  10540  expnbnd  10599  bccmpl  10688  fihashss  10751  leisorel  10772  shftfibg  10784  mulreap  10828  abssubne0  11055  maxleast  11177  lemininf  11197  ltmininf  11198  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  xrmineqinf  11232  xrltmininf  11233  xrminltinf  11235  xrminadd  11238  climuni  11256  reccn2ap  11276  isumz  11352  fsumsplitsnun  11382  geoisum1c  11483  prod1dc  11549  efltim  11661  dvdscmulr  11782  dvdsmulcr  11783  summodnegmod  11784  modmulconst  11785  dvdsmultr2  11795  dvdsexp  11821  mulmoddvds  11823  modremain  11888  divgcdz  11926  gcdaddm  11939  dvdsgcdb  11968  gcdass  11970  mulgcd  11971  gcddiv  11974  rplpwr  11982  uzwodc  11992  lcmdvdsb  12038  lcmass  12039  mulgcddvds  12048  qredeq  12050  qredeu  12051  rpmul  12052  divgcdcoprmex  12056  cncongr1  12057  rpexp  12107  rpexp12i  12109  odzcllem  12196  odzdvds  12199  odzphi  12200  pythagtriplem15  12232  pcpremul  12247  pcdiv  12256  pcqmul  12257  pcqdiv  12261  dvdsprmpweq  12288  sumhashdc  12299  pcfaclem  12301  qexpz  12304  ctinf  12385  setsvala  12447  ressid2  12477  ressval2  12478  rngbaseg  12534  grpasscan2  12763  grpidrcan  12764  grpidlcan  12765  2basgeng  12876  clsss  12912  ntrss  12913  ntrin  12918  neiss  12944  restco  12968  restabs  12969  lmconst  13010  psmetsym  13123  psmetge0  13125  xmetge0  13159  xmetsym  13162  xmetresbl  13234  mopni3  13278  bdxmet  13295  bdmopn  13298  txmetcnp  13312  dvfvalap  13444  dvid  13456  dvcnp2cntop  13457  ptolemy  13539  rpcxpadd  13620  rpmulcxp  13624  rpdivcxp  13626  cxpmul  13627  rpcxple2  13632  rpcxplt2  13633  cxpcom  13651  rplogbval  13657  rplogbcl  13658  rprelogbmulexp  13668  relogbexpap  13670  logbleb  13673  logblt  13674  rplogbcxp  13675  rpcxplogb  13676  lgslem1  13695  lgsfcl2  13701  lgsneg  13719  lgsne0  13733  lgssq2  13736  lgsdirnn0  13742