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 ⊢ (𝜑 → 𝜓)

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:  mt3i  150  olcnd  890  disjss3  5112  nnsuc  7880  poxp2  8139  frrlem14  8296  unxpdomlem2  9217  oismo  9502  cnfcom3lem  9672  rankelb  9796  fin33i  10353  isf34lem4  10361  canthp1lem2  10638  gchdju1  10641  pwfseqlem3  10645  inttsk  10759  r1tskina  10767  nqereu  10914  zbtwnre  12970  discr1  14275  seqcoll2  14502  bitsfzo  16493  bitsf1  16504  eucalglt  16643  4sqlem17  17021  4sqlem18  17022  ramubcl  17078  psgnunilem5  19564  odnncl  19615  gexnnod  19658  sylow1lem1  19668  torsubg  19924  prmcyg  19964  ablfacrplem  20137  pgpfac1lem2  20147  pgpfac1lem3a  20148  pgpfac1lem3  20149  xrsdsreclblem  21532  prmirredlem  21591  ppttop  23133  pptbas  23134  regr1lem  23865  alexsublem  24170  reconnlem1  24953  metnrmlem1a  24985  vitalilem4  25739  vitalilem5  25740  itg2gt0  25888  rollelem  26117  lhop1lem  26141  coefv0  26374  plyexmo  26443  lgamucov  27168  ppinprm  27282  chtnprm  27284  lgsdir  27462  lgseisenlem1  27505  2sqlem7  27554  2sqblem  27561  pntpbnd1  27716  madebdaylemlrcut  28058  bdayfinbndlem1  28626  dfon2lem8  36179  poimirlem25  38184  fdc  38284  ac6s6  38711  2atm  40191  llnmlplnN  40203  trlval3  40851  cdleme0moN  40889  cdleme18c  40957  qirropth  43527  aacllem  50475