Theorem mpani 698

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpani	|- (ph -> (ch -> th))

Proof of Theorem mpani

Step	Hyp	Ref	Expression
1		mpani.1	. 2 |- ps
2		mpani.2	. . 3 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 375	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpi 44	1 |- (ph -> (ch -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mp2ani 700  mpanr1 709  oeordi 4214  mulgt1t 5845  recgt1it 5900  recrecltt 5902  nngt0t 5946  nnrecgt0t 5953  xrub 6080  recnzt 6191  expordit 6600  expubndt 6608  expnbndt 6654  expnlbndt 6655  expcnvlem1 7227  georeclim 7240  geoisumr 7243  ivthlem7 7287  efaddlem16 7353  sin02gt0 7478  znnen 7502  minveclem25 8569  sinq12gt0t 8708  shftefif1olem 8741  shsubcltOLD 9090  dmdbr2 10230  cayleylem2 10410

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

Copyright terms: Public domain