Theorem mp3an12 908

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3an12	|- (ch -> th)

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 |- ps
2		mp3an12.1	. . 3 |- ph
3		mp3an12.3	. . 3 |- ((ph /\ ps /\ ch) -> th)
4	2, 3	mp3an1 905	. 2 |- ((ps /\ ch) -> th)
5	1, 4	mpan 697	1 |- (ch -> th)

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  tfi 3132  peano5 3159  fopabco 3838  fopabcos 3839  ndmopr 4051  oneo 4218  renegcl 5428  ltne 5595  ltm1t 5817  mulgt1t 5847  recgt1it 5902  recrecltt 5904  nnge1t 5945  nngt0t 5948  nnrecgt0t 5955  nnaddm1clt 5960  nnunb 6072  xrub 6082  recnzt 6193  uzrdgval 6303  icounlem 6413  eluzsubi 6438  expordit 6601  expubndt 6609  expnbndt 6655  expnlbndt 6656  imret 6774  imcjt 6819  faclbnd4lem1 6948  bcpasc 6969  infcvglem3 7223  expcnvlem1 7227  georeclim 7240  geoisumr 7243  cvgratlem2ALT 7248  ivthlem7 7287  efcnlem2 7420  sin01bndlem2 7469  cos01bndlem2 7471  sin01gt0 7477  cos01gt0 7478  qdensere 7748  cnmetdval 7899  xplmi 7970  xplmi2 7971  xplm 7972  xpcn 7973  oprcn 7974  bopcnlem3 7980  fsumcnlem 7986  vafval 8218  smfval 8220  0vfval 8221  vsfval 8250  imsmetlem 8319  nmcnilem 8333  ipfval 8348  ip1cnilem6 8374  lnocoi 8414  nmoubi 8431  nmobndi 8434  nmounbi 8435  nmlno0lem 8449  nmlnoubi 8452  isblo3i 8457  blometi 8459  blocni 8461  blocn2 8464  ipasslem2 8487  ubthlem3 8527  ubthlem5 8529  ubthlem9 8533  ubthlem11 8535  ubthlem12 8536  ubthlem13 8537  minveclem5 8545  minveclem10 8550  minveclem14 8554  minveclem16 8556  minveclem17 8557  minveclem19 8559  minveclem20 8560  minveclem22 8562  minveclem28 8568  minveclem35 8575  minveclem36 8576  minveclem37 8577  minveclem38 8578  htthlem8 8623  htthlem10 8625  sincolem 8660  sincosq1sgn 8699  sincosq3sgn 8701  sincosq4sgn 8702  sineq0 8708  hvsubidt 8890  hv2timest 8923  hi01t 8957  hhssabl 9127  pjsumt 9650  mayete3 9668  hoco 9685  hoaddid1 9707  honegsub 9717  honegnegt 9727  ho2timest 9740  nmopneg 9884  lnopco 9923  lnopeq 9928  adjbdlnb 10012  pjscj 10093  pjsspos 10095  pjssdif2 10097  mdsl2b 10245  cvmd 10246  mdslmd3 10254  mdslmd4 10255  mdexch 10257  cvat 10288  cvexchlem 10290  mdsym 10333  dmdbr5at 10344  domval 10626  codval 10627  idval 10628  cmpval 10629

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