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 716  mtbiri 717  exists2 1458  nsuceq0 3053  onssneli2 3102  unixp0 3518  funopg 3547  tz7.48-3 3958  tz7.49 3959  abianfp 3962  pwuninel 4486  2pwuninel 4487  ssrankr1 4676  rankxplim3 4714  zorn2lem4 4791  zorn2lem7 4794  carduni 4858  alephle 4884  alephfp 4900  nd1 4938  nd2 4939  axunnd 4948  nnunb 6070  indstr 6461  climunii 7098  efne0t 7369  infdif 7568  hlimunii 9108  hon0 9719  fiiu 10453  fiiuOLD 10454  fiiu2 10488  fiiu2OLD 10489

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

Copyright terms: Public domain