Theorem mp3an23 906

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 903	. 2 |- ((ph /\ ps) -> th)
5	1, 4	mpan2 695	1 |- (ph -> th)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  csbco3g 2036  sbcco3g 2037  nneob 4245  unfilem1 4530  abfii3 4543  1qec 5048  muleqaddt 5677  nnleltp1t 5909  halfclt 5988  rehalfclt 5989  half0t 5990  halfpos2t 5992  halfnneg2t 5993  lt0nnn0 6071  elnnz1 6110  zltp1let 6136  nneo 6152  zeot 6154  zneo 6155  zneoOLD 6156  dfuz 6158  ser1cl1 6275  icounlem 6353  seq0p1 6491  serzcl1 6502  sqrlem12 6622  fsum3 6970  fsum4 6971  binomlem5 7016  iserzex 7090  climserzle 7091  ser1const 7115  geoser 7177  geolimilem 7178  ivthlem1 7224  ivthlem4 7227  ivthlem9 7232  efaddlem1 7288  efaddlem16 7303  sinclt 7381  efi4pt 7385  resin4pt 7386  recos4pt 7387  sinnegt 7392  efivalt 7397  sinbndt 7415  cosbndt 7416  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  ruclem13 7473  tgioolem 7866  ipcl 8312  ipcj 8314  ip1cnilem6 8325  ipasslem11 8444  sincolem 8603  pilem1 8609  pilem2 8610  sincosq1lem 8639  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  efif1lem1 8664  efif1lem2 8665  hvmul0t 8832  pjthlem6 9162  pjthlem7 9163  h1de2b 9415  h1de2bOLD 9416  spanunsn 9442  nmopge0t 9774  nmfnge0t 9790  mdsl1 10185  mdsl2b 10187  mdexch 10199  superpos 10218  atabs 10265  dmdbr5at 10284  cdj3lem1 10295

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 776

Copyright terms: Public domain