Theorem mpan2d 704

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 376	. 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 4895  xrret 5581  xrre2t 5582  letrp1t 5818  ledivp1t 5907  xrltmint 5916  lemint 5923  xrinfmsslem 6079  peano2uz2 6203  uzind 6207  flget 6235  qbtwnxr 6280  monoord 6295  ser1add2 6339  ser1add 6340  elioc2t 6391  elico2t 6392  elicc2t 6393  fzss2t 6505  fsequb 6524  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 7889  metcnpi4 7890  metcni2 7892  bcthlem2 7997  nmoub3i 8432  minveceu 8579  shsel1t 9280  sumspansnt 9589  nmopub2tALT 9828  nmfnleub2t 9845

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