Theorem mp3an12 904

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

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  tfi 3121  peano5 3148  fopabco 3823  fopabcos 3824  oneo 4202  renegcl 5396  ltne 5564  ltm1t 5779  mulgt1t 5809  recgt1it 5856  recrecltt 5858  nnge1t 5899  nngt0t 5902  nnrecgt0t 5908  nnaddm1clt 5913  nnunb 6025  xrub 6035  recnzt 6146  uzrdgval 6247  icounlem 6353  eluzsubi 6377  expordit 6539  expubndt 6547  expnbndt 6593  imcjt 6762  faclbnd4lem1 6893  bcpasc 6915  infcvglem3 7166  expcnvlem1 7170  georeclim 7183  geoisumr 7186  cvgratlem2ALT 7191  ivthlem7 7230  ivthlem7OLD 7239  efcnlem2 7368  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  cos01gt0 7427  qdensere 7701  cnmetdval 7854  xplmi 7923  xplmi2 7924  xplm 7925  xpcn 7926  oprcn 7927  bopcnlem3 7933  fsumcnlem 7939  vafval 8174  smfval 8176  0vfval 8177  vsfval 8206  imsmetlem 8274  nmcnilem 8285  ipfval 8299  ip1cnilem6 8325  lnocoi 8365  nmoubi 8380  nmobndi 8383  nmounbi 8384  nmlno0lem 8398  nmlnoubi 8401  isblo3i 8405  blometi 8407  blocni 8409  blocn2 8412  ipasslem2 8435  ubthlem3 8475  ubthlem5 8477  ubthlem9 8481  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  minveclem5 8493  minveclem10 8498  minveclem14 8502  minveclem16 8504  minveclem17 8505  minveclem19 8507  minveclem20 8508  minveclem22 8510  minveclem28 8516  minveclem35 8523  minveclem36 8524  minveclem37 8525  minveclem38 8526  htthlem8 8570  htthlem10 8572  sincolem 8603  sincosq1sgn 8640  sincosq3sgn 8642  sincosq4sgn 8643  hvsubidt 8834  hv2timest 8867  hi01t 8901  hhssabl 9071  pjsumt 9595  mayete3 9613  hoco 9630  hoaddid1 9652  honegsub 9662  honegnegt 9672  ho2timest 9685  nmopneg 9828  lnopco 9866  lnopeq 9871  adjbdlnb 9955  pjscj 10036  pjsspos 10038  pjssdif2 10040  mdsl2b 10187  cvmd 10188  mdslmd3 10196  mdslmd4 10197  mdexch 10199  cvat 10230  cvexchlem 10232  mdsym 10275  dmdbr5at 10284  domval 10535  codval 10536  idval 10537  cmpval 10538

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