Theorem mtoi 199

Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)

Hypotheses

Ref	Expression
mtoi.1	⊢ ¬ 𝜒
mtoi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mtoi	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. . 3 ⊢ ¬ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → ¬ 𝜒)
3		mtoi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mtod 198	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  326  mtbiri  327  sbn1  2113  axc10  2389  pwnss  5293  nsuceq0  6408  onssnel2i  6441  abnex  7711  ssonprc  7741  soseq  8109  dmtpos  8188  tfrlem15  8331  tz7.44-2  8346  tz7.48-3  8383  2pwuninel  9070  2pwne  9071  nnsdomg  9209  r111  9699  r1pwss  9708  wfelirr  9749  rankxplim3  9805  carduni  9905  alephle  10010  alephfp  10030  pwdjudom  10137  cfsuc  10179  fin23lem28  10262  fin23lem30  10264  isfin1-2  10307  ac5b  10400  zorn2lem4  10421  zorn2lem7  10424  cfpwsdom  10507  nd1  10510  nd2  10511  canthp1  10577  pwfseqlem1  10581  gchhar  10602  winalim2  10619  ltxrlt  11216  recgt0  12001  nnunb  12433  indstr  12866  wrdlen2i  14904  rlimno1  15616  lcmfnncl  16598  isprm2  16651  nprmdvds1  16676  divgcdodd  16680  coprm  16681  ramtcl2  16982  chnccat  18592  psgnunilem3  19471  torsubg  19829  prmcyg  19869  dprd2da  20019  prmirredlem  21452  pnfnei  23185  mnfnei  23186  1stccnp  23427  uzfbas  23863  ufinffr  23894  fin1aufil  23897  ovolunlem1a  25463  itg2gt0  25727  lgsquad2lem2  27348  dirith2  27491  noseponlem  27628  nosepssdm  27650  nodenselem8  27655  nolt02o  27659  nogt01o  27660  umgrnloop0  29178  usgrnloop0ALT  29274  nfrgr2v  30342  hon0  31864  ifeqeqx  32612  axsepg2ALT  35226  dfon2lem7  35969  bj-axc10v  37100  sbn1ALT  37165  bj-nsnid  37377  areacirclem4  38032  fdc  38066  dihglblem6  41786  sn-itrere  42933  sn-retire  42934  pellexlem6  43262  pw2f1ocnv  43465  wepwsolem  43470  inaex  44724  axc5c4c711toc5  44829  lptioo2  46061  lptioo1  46062  1neven  48714