Theorem mp2and 702

Description: A deduction based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp2and	|- (ph -> th)

Proof of Theorem mp2and

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 |- (ph -> ch)
2		mp2and.1	. . 3 |- (ph -> ps)
3		mp2and.3	. . 3 |- (ph -> ((ps /\ ch) -> th))
4	2, 3	mpand 700	. 2 |- (ph -> (ch -> th))
5	1, 4	mpd 26	1 |- (ph -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  tfindsg2 3158  letrd 5507  lelttrd 5508  ltletrd 5509  lttrd 5510  ltmul12it 5805  zltp1let 6136  uzind 6161  ioossicc 6338  uztrn 6368  elfzle3 6425  fsequb 6463  faclbnd3 6892  fsumcmp 6986  fsumabs 6989  climmullem3 7066  climmullem4 7067  climmullem5 7068  ivthlem6 7229  ivthlem6OLD 7238  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  infxpidmlem12 7514  xpcn 7926  subgid 8072  nmoge0 8375  isblo3i 8405  ubthlem11 8483  sinq12gt0t 8644  eff1i 8683  nmopge0t 9774  nmfnge0t 9790  nmoptri 9965  stadd 10111  stadd3 10113  atcvatlem 10249  ghomgsg 10329  iri 10608

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