Theorem mtoi 122

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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  mtbii 784  mtbiri 785  ax4 1318  exists2OLD 1864  eunex 3500  nsuceq0 3749  onssnel2i 3780  unixp0 4423  funopg 4454  tz7.48-3 5167  tz7.49 5168  abianfp 5171  pwuninel 5550  2pwuninel 5551  pwne 5552  2pwne 5553  ordtypelem4 5687  ssrankr1 5787  rankxplim3 5825  omsubsuc2 5878  zorn2lem4 5953  zorn2lem7 5956  carduni 6010  alephle 6032  alephfp 6048  nd1 6090  nd2 6091  axunnd 6100  nnunb 7279  indstr 7630  climunii 8358  efne0 8631  infdif 8837  indexfi 10174  fiuni 10219  fiiu2 10220  hlimuniii 10741  hon0 11356  isprm2 13775  coprm 13782  dfon2lem7 13855  soseq 13955  axdenselem8 14026  fiiu 14344  unpde2eg22 14407  elfiun 15369  ordtypelem4OLD 15378  omsubsuc2OLD 15387  indexfiOLD 15755  inficl 15757  fdc 15812  heiborlem11 15965  heiborlem13 15967

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

Copyright terms: Public domain