Theorem simp3 906

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

Assertion

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

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 903	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )
2	1	simprd 107	1 |- ( ( ph /\ ps /\ ch ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 885

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

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

This theorem is referenced by:  simpl3  909  simpr3  912  simp3i  915  simp3d  918  simp13  936  simp23  939  simp33  942  3anibar  1072  3ianorr  1204  stoic4a  1321  stoic4b  1322  mob2  2721  sotri2  4722  sotri3  4723  feq123  5038  resasplitss  5069  sefvex  5196  ftpg  5347  fsnunf  5362  fnfvima  5393  cocan1  5427  cocan2  5428  f1oiso2  5466  riotass  5495  moriotass  5496  ovmpt2x  5629  ovmpt2ga  5630  caovimo  5694  ofrval  5722  dfsmo2  5902  nnsucsssuc  6071  f1oen2g  6235  f1dom2g  6236  xpdom3m  6308  diffifi  6351  mulcanenq  6483  ltanqg  6498  addnnnq0  6547  nnanq0  6556  prltlu  6585  distrprg  6686  ltexprlemm  6698  recexprlem1ssl  6731  recexprlem1ssu  6732  addsrpr  6830  mulsrpr  6831  mulasssrg  6843  recexgt0sr  6858  axmulass  6947  axpre-ltadd  6960  ltxrlt  7085  subadd2  7215  addsubass  7221  nppcan  7233  nppcan3  7235  subcan2  7236  subsub2  7239  subsub4  7244  pnpcan  7250  pnncan  7252  subcan  7266  subdi  7382  ltadd1  7424  leadd1  7425  leadd2  7426  ltsubadd  7427  ltsubadd2  7428  lesubadd  7429  lesubadd2  7430  ltaddsub  7431  leaddsub  7433  lesub1  7451  lesub2  7452  ltsub1  7453  ltsub2  7454  ltaddsublt  7562  gt0add  7564  reapadd1  7587  remulext1  7590  remulext2  7591  apadd2  7600  mulext2  7604  mulap0r  7606  leltap  7615  ltap  7622  divap0b  7662  divcanap5  7690  dmdcanap  7698  redivclap  7707  div2negap  7711  lt2msq1  7851  ltdiv2  7853  nndivtr  7955  gtndiv  8335  eluzsub  8502  nn01to3  8552  qdivcl  8577  irrmul  8581  rpgecl  8611  divge1  8649  ubioog  8783  ubioc1  8798  lbico1  8799  iccleub  8800  lbicc2  8852  ubicc2  8853  icoshftf1o  8859  fzen  8907  elfz1b  8952  uznfz  8965  elfzo0  9038  elfzo0z  9040  ubmelfzo  9056  fzonn0p1p1  9069  ubmelm1fzo  9082  qbtwnre  9111  flqwordi  9130  flltdivnn0lt  9146  ceiqle  9155  modqval  9166  modqvalr  9167  modqcl  9168  flqpmodeq  9169  modq0  9171  mulqmod0  9172  negqmod0  9173  modqge0  9174  modqlt  9175  modqdiffl  9177  modqdifz  9178  modqmulnn  9184  frec2uzf1od  9192  expnegap0  9263  expgt1  9293  exprecap  9296  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  expnbnd  9372  shftfibg  9421  redivap  9474  imdivap  9481  cjdivap  9509  climuni  9814