Theorem mp2and 707

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  tfindsg2 3214  letrd 5680  lelttrd 5681  ltletrd 5682  lttrd 5683  ltmul12a 5985  zltp1le 6349  uzind 6376  ioossicc 6524  uztrn 6555  elfzle3 6613  fsequb 6654  faclbnd3 7150  fsumcmp 7243  fsumabs 7246  climmullem3 7325  climmullem4 7326  climmullem5 7327  ivthlem6 7491  sin01gt0 7685  cos01gt0 7686  sin02gt0 7687  infxpidmlem12 7775  xpcn 8187  subgid 8362  nmoge0 8684  isblo3i 8716  ubthlem11 8797  sinq12gt0t 8975  eff1i 9016  nmopge0 10115  nmfnge0 10131  nmoptrii 10306  staddi 10454  stadd3i 10456  atcvatlem 10594  ghomgsg 10680  stoig 11064  iri 11255  idsubfun 11312  alexsublem1 11496  cnconn 11503  fbssint 11626  ufileu 11658  filufint 11659  limfilcf 11683  dirtr 11753  fimax 11837  txcn 11979  ismtyhmeolem 12006  heiborlem32 12042  iccbnd 12082

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 145  df-an 223

Copyright terms: Public domain