Theorem mtoi 107

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 95	. 2 |- (ph -> (-. ch -> -. ps))
4	1, 3	mpi 44	1 |- (ph -> -. ps)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  mtbii 714  mtbiri 715  exists2 1451  nsuceq0 3043  onssneli2 3092  unixp0 3504  funopg 3533  tz7.48-3 3943  tz7.49 3944  abianfp 3947  pwuninelg 4467  ssrankr1 4648  rankxplim3 4686  zorn2lem4 4763  zorn2lem7 4766  carduni 4830  alephle 4856  alephfp 4872  nd1 4910  nd2 4911  axunnd 4920  nnunb 6017  indstr 6393  climunii 7035  efne0t 7311  infdif 7511  hlimunii 9029  hon0 9636  fiiu 10350  fiiu2 10377

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

Copyright terms: Public domain