Theorem mpan2d 706

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 374	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpid 47	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  alephle 5034  xrre 5723  xrre2 5724  letrp1 5956  ledivp1 6050  xrltmin 6059  lemin 6066  xrinfmsslem 6245  peano2uz2 6372  uzind 6376  qbtwnxr 6419  flge 6431  monoord 6482  elioc2 6516  elico2 6517  elicc2 6518  fzss2 6634  fsequb 6654  ser1add2i 6703  ser1addi 6704  leabs 7066  seq1bndi 7113  cvg2i 7125  caubndi 7129  facwordi 7147  facavg 7158  clm4lei 7284  2climnn 7305  2climnn0 7306  climmullem5 7327  ser1cmp2lem 7379  ivthlem6 7491  ivthlem7 7492  metcnpi3 8103  metcnpi4 8104  metcni2 8106  bcthlem2 8211  vacnlem3 8584  nmoub3i 8690  minveceu 8843  shsel1 9561  sumspansn 9872  nmopub2tALT 10113  nmfnleub2 10130  fixp 11840  incsequz 11879  txcn 11979  heiborlem32 12042

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