Theorem mp2and 703

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 701	. 2 |- (ph -> (ch -> th))
5	1, 4	mpd 26	1 |- (ph -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  tfindsg2 3163  letrd 5526  lelttrd 5527  ltletrd 5528  lttrd 5529  ltmul12it 5841  zltp1let 6181  uzind 6205  ioossicc 6397  uztrn 6428  elfzle3 6485  fsequb 6523  faclbnd3 6947  fsumcmp 7040  fsumabs 7043  climmullem3 7122  climmullem4 7123  climmullem5 7124  ivthlem6 7286  sin01gt0 7476  cos01gt0 7477  sin02gt0 7478  infxpidmlem12 7563  xpcn 7976  subgid 8120  nmoge0 8430  isblo3i 8461  ubthlem11 8539  sinq12gt0t 8708  eff1i 8744  nmopge0t 9835  nmfnge0t 9851  nmoptri 10027  stadd 10173  stadd3 10175  atcvatlem 10312  ghomgsg 10395  unpde2eg2 10544  iri 10728

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