Theorem mp3an12 912

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 909	. 2 |- ((ps /\ ch) -> th)
5	1, 4	mpan 699	1 |- (ch -> th)

Syntax hints:   -> wi 3   /\ w3a 781

This theorem is referenced by:  tfi 3207  peano5 3241  fopabco 3946  fopabcos 3947  ndmopr 4106  oneo 4348  renegcli 5570  ltnei 5737  mul0ori 5846  divasszi 5891  ltm1 5955  ltmul2i 5977  mulgt1 5989  recgt1i 6045  recreclt 6047  ltdivp1i 6052  nnge1 6088  nngt0 6091  nnrecgt0 6099  nnaddm1cl 6104  nnunb 6238  xrub 6248  recnz 6362  icounlem 6539  eluzsubi 6564  uzrdgvali 6666  expordi 6797  expubnd 6805  expnbnd 6852  expnlbnd 6853  expnlbnd2 6854  imre 6974  imcj 7020  abs1mi 7107  faclbnd4lem1 7151  bcpasci 7172  infcvglem3 7427  expcnvlem1 7431  georeclim 7445  geoisumr 7448  0.999... 7451  cvgratlem2ALT 7453  ivthlem7 7492  efcnlem2 7628  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  cos01gt0 7686  absefib 7693  efieq1re 7694  qdensere 7961  cnmetdval 8113  xplmi 8184  xplmi2 8185  xplm 8186  xpcn 8187  oprcn 8188  bopcnlem3 8194  fsumcnlem 8200  bcthlem1 8210  bcthlem21 8230  vafval 8469  smfval 8471  0vfval 8472  vsfval 8501  imsmetlem 8570  vacnlem3 8584  vacnlem6 8587  nmcnilem 8591  ipfval 8606  ip1cnilem6 8632  lnocoi 8672  nmoubi 8689  nmobndi 8692  nmounbi 8693  nmlno0lem 8708  nmlnoubi 8711  isblo3i 8716  blometi 8718  blocni 8720  blocn2 8723  ipasslem2 8747  siii 8769  ubthlem3 8789  ubthlem5 8791  ubthlem9 8795  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  minveclem5 8809  minveclem10 8814  minveclem14 8818  minveclem16 8820  minveclem17 8821  minveclem19 8823  minveclem20 8824  minveclem22 8826  minveclem28 8832  minveclem35 8839  minveclem36 8840  minveclem37 8841  minveclem38 8842  htthlem8 8889  htthlem10 8891  sincolem 8932  sincosq1sgn 8971  sincosq3sgn 8973  sincosq4sgn 8974  sineq0 8983  sineq0OLD 8984  sineq0re 8985  hvsubid 9170  hv2times 9203  hi01 9238  hhssabli 9408  pjsumi 9933  mayete3i 9951  mayete3OLDi 9952  hocoi 9970  hoaddid1i 9992  honegsubi 10002  honegneg 10012  ho2times 10025  eigorthi 10043  nmopnegi 10168  lnopcoi 10207  lnopeqi 10212  adjbdlnb 10296  pjscji 10378  pjssposi 10380  pjssdif2i 10382  mdsl2bi 10531  cvmdi 10532  mdslmd3i 10540  mdslmd4i 10541  mdexchi 10543  cvati 10574  cvexchlem 10576  mdsymi 10620  dmdbr5ati 10631  sbtpsines 11062  domval 11177  codval 11178  idval 11179  cmpval 11180  finminlem 11418  reconnlem1 11507  rddif 11869  absrdbnd 11870  elnnr 11874  heiborlem15 12025  heiborlem23 12033  bfplem8 12061  bfplem9 12062

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 145  df-an 223  df-3an 783

Copyright terms: Public domain