Theorem mpan2d 702

Description: A deduction based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpan2d	|- (ph -> (ps -> th))

Proof of Theorem mpan2d

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 |- (ph -> ch)
2		mpan2d.2	. . 3 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 375	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpid 47	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  alephle 4884  xrret 5569  xrre2t 5570  letrp1t 5816  ledivp1t 5905  xrltmint 5914  lemint 5921  xrinfmsslem 6077  peano2uz2 6201  uzind 6205  flget 6233  qbtwnxr 6279  monoord 6294  ser1add2 6338  ser1add 6339  elioc2t 6390  elico2t 6391  elicc2t 6392  fzss2t 6504  fsequb 6523  leabst 6864  seq1bnd 6910  cvg2 6922  caubnd 6926  facwordit 6944  facavgt 6955  clm4le 7081  2climnn 7102  2climnn0 7103  climmullem5 7124  ser1cmp2lem 7176  ivthlem6 7286  ivthlem7 7287  metcnpi3 7892  metcnpi4 7893  metcni2 7895  bcthlem2 8000  nmoub3i 8436  minveceu 8583  spwpr3OLD 8662  shsel1t 9285  sumspansnt 9594  nmopub2tALT 9833  nmfnleub2t 9850

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