Theorem con1d 145

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 142	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 35	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 115	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:  con1  146  mt3d  148  pm2.24d  151  con3d  152  pm2.61d  179  pm2.8  969  dedlem0b  1041  meredith  1645  necon3bd  2955  necon1bd  2959  spc2d  3536  sspss  4035  neldif  4065  ssonprc  7619  limsssuc  7677  limom  7708  onfununi  8148  pw2f1olem  8821  domtriord  8864  pssnn  8905  pssnnOLD  8986  ordtypelem10  9232  rankxpsuc  9587  carden2a  9671  fidomtri2  9699  alephdom  9784  isf32lem12  10067  isfin1-3  10089  isfin7-2  10099  entric  10260  inttsk  10477  zeo  12352  zeo2  12353  xrlttri  12818  xaddf  12903  elfzonelfzo  13433  fzonfzoufzol  13434  elfznelfzo  13436  om2uzf1oi  13617  hashnfinnn0  14020  ruclem3  15886  sumodd  16041  bitsinv1lem  16092  sadcaddlem  16108  phiprmpw  16421  iserodd  16480  fldivp1  16542  prmpwdvds  16549  vdwlem6  16631  sylow2alem2  19167  efgs1b  19286  fctop  22098  cctop  22100  ppttop  22101  iccpnfcnv  24051  iccpnfhmeo  24052  iscau2  24384  ovolicc2lem2  24625  mbfeqalem1  24748  limccnp2  24999  radcnv0  25518  psercnlem1  25527  pserdvlem2  25530  logtayl  25758  cxpsqrt  25801  rlimcnp2  26059  amgm  26083  pntpbnd1  26677  pntlem3  26700  atssma  30681  fsuppcurry1  31002  fsuppcurry2  31003  supxrnemnf  31033  xrge0iifcnv  31825  eulerpartlemf  32279  cusgracyclt3v  33060  nolesgn2o  33843  nogesgn1o  33845  arg-ax  34574  pw2f1ocnv  40817  infordmin  41079  clsk1independent  41587  pm10.57  41920  con5  42073  con3ALT2  42081  xrred  42836  afvco2  44597  islininds2  45755