Theorem simp1 904

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

Assertion

Ref	Expression
simp1	|- ( ( ph /\ ps /\ ch ) -> ph )

Proof of Theorem simp1

Step	Hyp	Ref	Expression
1		3simpa 901	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simpld 105	1 |- ( ( ph /\ ps /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ w3a 885

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

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simpl1  907  simpr1  910  simp1i  913  simp1d  916  simp11  934  simp21  937  simp31  940  syld3an3  1180  3ianorr  1204  stoic4a  1321  stoic4b  1322  rsp2e  2372  issod  4056  elirr  4266  sotri2  4722  sotri3  4723  funtpg  4950  funimaexglem  4982  feq123  5038  foco2  5318  ftpg  5347  fsnunf  5362  fcofo  5424  f1oiso2  5466  riotass  5495  ovmpt2x  5629  ovmpt2ga  5630  caovimo  5694  ofeq  5714  ofrval  5722  frecsuclem3  5990  diffifi  6351  mulcanenq  6483  ltanqg  6498  addnnnq0  6547  distrlem4prl  6682  distrlem4pru  6683  distrprg  6686  aptipr  6739  addsrpr  6830  mulsrpr  6831  mulasssrg  6843  axmulass  6947  axpre-ltadd  6960  mul31  7144  addsubass  7221  subcan2  7236  subsub2  7239  subsub4  7244  npncan3  7249  pnpcan  7250  pnncan  7252  subcan  7266  subdi  7382  ltadd1  7424  leadd1  7425  leadd2  7426  ltsubadd  7427  lesubadd  7429  ltaddsub  7431  leaddsub  7433  lesub1  7451  lesub2  7452  ltsub1  7453  ltsub2  7454  ltaddsublt  7562  gt0add  7564  apreap  7578  lemul1  7584  reapmul1lem  7585  reapmul1  7586  reapadd1  7587  remulext1  7590  remulext2  7591  apadd2  7600  mulext2  7604  mulap0r  7606  leltap  7615  ltap  7622  recexaplem2  7633  mulcanap  7646  mulcanap2  7647  divvalap  7653  divcanap2  7659  diveqap0  7661  divrecap  7667  divrecap2  7668  divdirap  7674  divcanap3  7675  div11ap  7677  divcanap5  7690  redivclap  7707  div2negap  7711  apmul1  7764  ltdiv1  7834  ltmuldiv  7840  lemuldiv  7847  lt2msq1  7851  ltdiv23  7858  lediv23  7859  squeeze0  7870  gtndiv  8335  eluz2  8479  eluzsub  8502  peano2uz  8526  nn01to3  8552  divge1  8649  ledivge1le  8652  ixxssixx  8771  lbico1  8799  lbicc2  8852  icoshftf1o  8859  fzen  8907  fzrev3  8949  fzrevral2  8968  elfzo0  9038  elfzo0z  9040  fzosplitprm1  9090  qbtwnre  9111  flqwordi  9130  flqword2  9131  adddivflid  9134  flltdivnn0lt  9146  modqcl  9168  mulqmod0  9172  modqmulnn  9184  iseqeq2  9215  iseqeq3  9216  expnegap0  9263  expgt1  9293  exprecap  9296  leexp2a  9307  expubnd  9311  sqdivap  9318  expnbnd  9372  shftfibg  9421  mulreap  9464  abssubne0  9687  climuni  9814