Theorem pm2.61d 127

Description: Deduction eliminating an antecedent.

Hypotheses

Ref	Expression
pm2.61d.1	|- (ph -> (ps -> ch))
pm2.61d.2	|- (ph -> (-. ps -> ch))

Assertion

Ref	Expression
pm2.61d	|- (ph -> ch)

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.1	. . 3 |- (ph -> (ps -> ch))
2	1	com12 11	. 2 |- (ps -> (ph -> ch))
3		pm2.61d.2	. . 3 |- (ph -> (-. ps -> ch))
4	3	com12 11	. 2 |- (-. ps -> (ph -> ch))
5	2, 4	pm2.61i 126	1 |- (ph -> ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61d1 128  pm2.61d2 129  pm2.61dan 477  a12stdy4 1375  pm2.61dne 1635  ordsson 2991  ordunidif 3005  findsg 3157  tfindsg 3162  fvco 3774  dff2 3817  omwordi 4202  omass 4211  eceqopreq 4313  pssnn 4534  unxpdomlem 4843  prlem936 5155  ssgt0sr 5217  suppsr2 5223  suppsr3 5224  elcncf 7265  cnconst 7780  atdmd 10325  atmd2 10327  mdsymlem4 10333

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain