Theorem mtoi 94

Description: Modus tollens inference.

Hypotheses

Ref	Expression
mtoi.1	|- -. ch
mtoi.2	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
mtoi	|- (ph -> -. ps)

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. 2 |- -. ch
2		mtoi.2	. . 3 |- (ph -> (ps -> ch))
3	2	con3d 87	. 2 |- (ph -> (-. ch -> -. ps))
4	1, 3	mpi 44	1 |- (ph -> -. ps)

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  mtbii 538  mtbiri 539  nbn 542  exists2 1073  nsuceq0 2306  onssneli2 2350  tz7.48-3 2996  tz7.49 2997  abianfp 3000  ssrankr1 3520  zornlem4 3606  zornlem7 3609  carduni 3664  alephle 3689  nd1 3732  nd2 3733  axunnd 3742  nnunb 4520  indstr 4611  climunii 4883  infdif 4948  hlimunii 5143

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

metamath.org