Theorem mt3d 149

Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)

Hypotheses

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

Assertion

Ref	Expression
mt3d	⊢ (𝜑 → 𝜓)

Proof of Theorem mt3d

Step	Hyp	Ref	Expression
1		mt3d.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mt3d.2	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
3	2	con1d 146	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
4	1, 3	mpd 16	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt3i  150  olcnd  891  disjss3  5102  nnsuc  7884  poxp2  8144  frrlem14  8301  unxpdomlem2  9232  oismo  9518  cnfcom3lem  9688  rankelb  9814  fin33i  10428  isf34lem4  10436  canthp1lem2  10719  gchdju1  10722  pwfseqlem3  10726  inttsk  10840  r1tskina  10848  nqereu  10995  zbtwnre  13054  discr1  14363  seqcoll2  14590  bitsfzo  16585  bitsf1  16596  eucalglt  16740  4sqlem17  17119  4sqlem18  17120  ramubcl  17176  psgnunilem5  19688  odnncl  19739  gexnnod  19782  sylow1lem1  19792  torsubg  20048  prmcyg  20088  ablfacrplem  20261  pgpfac1lem2  20271  pgpfac1lem3a  20272  pgpfac1lem3  20273  xrsdsreclblem  21699  prmirredlem  21758  ppttop  23305  pptbas  23306  regr1lem  24038  alexsublem  24343  reconnlem1  25126  metnrmlem1a  25158  vitalilem4  25912  vitalilem5  25913  itg2gt0  26061  rollelem  26289  lhop1lem  26313  coefv0  26547  plyexmo  26618  lgamucov  27347  chtnprm  27463  lgsdir  27641  lgseisenlem1  27684  2sqlem7  27733  2sqblem  27740  pntpbnd1  27895  madebdaylemlrcut  28267  bdayfinbndlem1  28835  dfon2lem8  36522  poimirlem25  38531  fdc  38647  ac6s6  39072  2atm  40552  llnmlplnN  40564  trlval3  41212  cdleme0moN  41250  cdleme18c  41318  qirropth  43868  aacllem  50883