Theorem mp3an23 910

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an23.1	|- ps
mp3an23.2	|- ch
mp3an23.3	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an23	|- (ph -> th)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 |- ps
2		mp3an23.2	. . 3 |- ch
3		mp3an23.3	. . 3 |- ((ph /\ ps /\ ch) -> th)
4	2, 3	mp3an3 907	. 2 |- ((ph /\ ps) -> th)
5	1, 4	mpan2 698	1 |- (ph -> th)

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  csbco3g 2043  sbcco3g 2044  nneob 4261  unfilem1 4560  1qec 5080  muleqaddt 5712  nnleltp1t 5956  halfclt 6035  rehalfclt 6036  half0t 6037  halfpos2t 6039  halfnneg2t 6040  2halvest 6041  halfaddsubt 6043  lt0nnn0 6118  elnnz1 6157  zltp1let 6183  nneo 6199  zeot 6201  zneo 6202  dfuz 6204  flhalft 6248  ser1cl1 6331  icounlem 6413  seq0p1 6552  serzcl1 6563  sqrlem12 6685  imcjt 6819  absmaxt 6897  fsum3 7024  fsum4 7025  binomlem5 7070  climaddlem3 7116  iserzex 7146  climserzle 7147  ser1const 7171  geoser 7234  geolimilem 7235  ivthlem1 7281  ivthlem4 7284  ivthlem9 7289  efaddlem1 7338  efaddlem16 7353  sinclt 7431  efi4pt 7435  resin4pt 7436  recos4pt 7437  sinnegt 7442  efivalt 7447  sinbndt 7466  cosbndt 7467  sin01bndlem2 7469  sin01bndlem3 7470  cos01bndlem2 7471  cos01bndlem3 7472  sin01gt0 7477  cos01gt0 7478  sin02gt0 7479  ruclem13 7523  ioo2bl 7909  tgioolem 7911  4ipval2 8354  4ipval3 8358  ipid 8359  ipcl 8361  ipcj 8363  ip1cnilem6 8374  ipasslem11 8496  minveclem27 8567  sincolem 8660  pilem1 8666  pilem2 8667  sinkpi 8692  sincosq1lem 8698  sincosq2sgn 8700  sincosq3sgn 8701  sincosq4sgn 8702  sinq12gt0t 8703  abssinper 8707  sineq0 8708  efif1lem1 8725  efif1lem2 8726  hvmul0t 8888  pjthlem6 9219  pjthlem7 9220  h1de2b 9472  spanunsn 9497  nmopge0t 9830  nmfnge0t 9846  mdsl1 10243  mdsl2b 10245  mdexch 10257  superpos 10276  atabs 10323  dmdbr5at 10344  cdj3lem1 10356

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain