Theorem con1d 138

Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992.)

Hypothesis

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

Assertion

Ref	Expression
con1d	⊢ (𝜑 → (¬ 𝜒 → 𝜓))

Proof of Theorem con1d

Step	Hyp	Ref	Expression
1		con1d.1	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2		notnot 135	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 34	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 113	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:  mt3d  139  con1  142  pm2.24d  146  con3d  147  pm2.61d  169  pm2.8  891  dedlem0b  992  meredith  1557  axc11nlemOLD2  1975  axc16nf  2122  hbntOLD  2130  axc11nlemOLD  2146  axc11nlemALT  2294  necon3bd  2796  necon1bd  2800  sspss  3668  neldif  3697  ssonprc  6884  limsssuc  6942  limom  6972  onfununi  7325  pw2f1olem  7949  domtriord  7991  pssnn  8063  ordtypelem10  8315  rankxpsuc  8628  carden2a  8675  fidomtri2  8703  alephdom  8787  isf32lem12  9069  isfin1-3  9091  isfin7-2  9101  entric  9258  inttsk  9475  zeo  11339  zeo2  11340  xrlttri  11848  xaddf  11929  elfzonelfzo  12436  fzonfzoufzol  12437  elfznelfzo  12439  om2uzf1oi  12614  hashnfinnn0  13013  ruclem3  14801  sumodd  14949  bitsinv1lem  15001  sadcaddlem  15017  phiprmpw  15319  iserodd  15378  fldivp1  15439  prmpwdvds  15446  vdwlem6  15528  sylow2alem2  17856  efgs1b  17972  fctop  20618  cctop  20620  ppttop  20621  iccpnfcnv  22551  iccpnfhmeo  22552  iscau2  22883  ovolicc2lem2  23093  mbfeqalem  23215  limccnp2  23462  radcnv0  23974  psercnlem1  23983  pserdvlem2  23986  logtayl  24206  cxpsqrt  24249  leibpilem1  24467  rlimcnp2  24493  amgm  24517  pntpbnd1  25075  pntlem3  25098  atssma  28621  spc2d  28697  supxrnemnf  28924  xrge0iifcnv  29307  eulerpartlemf  29759  arg-ax  31585  pw2f1ocnv  36622  clsk1independent  37364  pm10.57  37592  con5  37749  con3ALT2  37757  xrred  38522  afvco2  39905  islininds2  42067