Theorem mpanr1 774

Description: An inference based on modus ponens. (The proof was shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
mpanr1	|- ((ph /\ ch) -> th)

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2 |- ps
2		mpanr1.2	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
3	2	anassrs 489	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpanl2 771	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mpanr12 778  mpanlr1 779  tfr3 5134  oacl 5215  omcl 5216  omclOLD 5217  oaordi 5227  oawordri 5232  oaass 5243  oarec 5244  omordi 5245  omwordri 5251  odi 5258  omass 5259  oeoelem 5273  noinfep 5747  axcnre 6439  divdiv23zi 6971  divgt0i 7039  divge0i 7040  ltdiv23i 7077  recp1lt1 7084  ltdivp1i 7090  crreczi 7991  absdivzi 8110  recvalzi 8139  climmullem1 8380  climmullem2 8381  climmullem3 8382  climmullem4 8383  cos01gt0 8743  metge0 9096  bopcnlem2 9260  vc2 9506  vc0 9520  vcm 9522  vcnegneg 9525  nvnncan 9615  nvpi 9626  nvge0 9634  sm1cnilem 9686  ipval3 9698  ipid 9702  sspmval 9731  minveclem30 9919  occllem6 10811  nmopcoadji 11671  opsqrlem1 11711  opsqrlem6 11716  hstle 11802  hstrbi 11838  atordi 11956  frfi 15771

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 164  df-an 242

Copyright terms: Public domain