Theorem mpani 696

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 698  mpanr1 707  oeordi 4198  mulgt1t 5801  recgt1it 5848  recrecltt 5850  nngt0t 5894  nnrecgt0t 5900  xrub 6027  recnzt 6138  expordit 6531  expubndt 6539  expnbndt 6585  expcnvlem1 7162  georeclim 7175  geoisumr 7178  ivthlem7 7222  ivthlem7OLD 7231  efaddlem16 7295  sin02gt0 7420  znnen 7445  minveclem25 8500  sinq12gt0t 8625  shftefif1olem 8661  shftefif1olemOLD 8662  shsubcltOLD 9011  dmdbr2 10140  cayleylem2 10317

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