Theorem mp2and 767

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  mpbi2and 801  mpbir2and 802  tfindsg2 3945  letrd 6696  lelttrd 6697  ltletrd 6698  lttrd 6699  ltmul12a 7023  zltp1le 7390  uzind 7417  ioossicc 7566  uztrn 7597  elfzle3 7655  fsequb 7702  faclbnd3 8199  fsumcmp 8300  fsumabs 8303  climmullem3 8382  climmullem4 8383  climmullem5 8384  ivthlem6 8548  sin01gt0 8742  cos01gt0 8743  sin02gt0 8744  infxpidmlem12 8832  xpcn 9254  subgid 9429  nmoge0 9769  isblo3i 9801  ubthlem11 9882  sinq12gt0t 10057  eff1i 10098  txcn 10227  stoig 10251  fbssint 10279  dirtr 10356  nmopge0 11472  nmfnge0 11488  nmoptrii 11664  staddi 11818  stadd3i 11820  atcvatlem 11957  bnj1098 12917  bnj1357 13082  bnj1108 13416  bnj1110 13417  bnj1121 13421  ghomgsg 13636  dfon2lem6 13854  dfon2lem8 13856  frxp 13951  iri 15149  idsubfun 15206  alexsublem1 15437  cnconn 15444  ufileu 15573  filufint 15574  limfilcf 15587  fimax 15746  ismtyhmeolem 15950  heiborlem32 15986  iccbnd 16026  latledi 16884  lubun 16899  lubunNEW 16900  omlfh1 16978  hlatmstc 17047  cvr1 17054  cvratlem 17061  ps2 17079  paddasslem5 17285  paddasslem12 17292  paddasslem13 17293

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 164  df-an 242

Copyright terms: Public domain