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 476  a12stdy4 1352  pm2.61dne 1611  ordsson 2954  ordunidif 2968  findsg 3120  tfindsg 3125  fvco 3713  dff2 3756  omwordi 4140  omass 4149  eceqopreq 4251  pssnn 4465  unxpdomlem 4766  prlem936 5078  ssgt0sr 5140  suppsr2 5146  suppsr3 5147  elcncf 7151  cnconst 7667  atdmd 10447  atmd2 10449  mdsymlem4 10455

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

Copyright terms: Public domain