Theorem mpani 697

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 699  mpanr1 708  oeordi 4204  mulgt1t 5809  recgt1it 5856  recrecltt 5858  nngt0t 5902  nnrecgt0t 5908  xrub 6035  recnzt 6146  expordit 6539  expubndt 6547  expnbndt 6593  expcnvlem1 7170  georeclim 7183  geoisumr 7186  ivthlem7 7230  ivthlem7OLD 7239  efaddlem16 7303  sin02gt0 7428  znnen 7453  minveclem25 8513  sinq12gt0t 8644  shftefif1olem 8680  shsubcltOLD 9029  dmdbr2 10168  cayleylem2 10344

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