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  974  dedlem0b  1044  meredith  1640  ax12ev2  2179  necon3bd  2945  necon1bd  2949  spc2d  3585  sspss  4082  neldif  4114  ssonprc  7789  limsssuc  7853  limom  7885  onfununi  8363  pw2f1olem  9098  domtriord  9145  pssnn  9190  ordtypelem10  9549  rankxpsuc  9904  carden2a  9988  fidomtri2  10016  alephdom  10103  isf32lem12  10386  isfin1-3  10408  isfin7-2  10418  entric  10579  inttsk  10796  zeo  12687  zeo2  12688  xrlttri  13163  xaddf  13248  elfzonelfzo  13790  fzonfzoufzol  13791  elfznelfzo  13793  om2uzf1oi  13976  hashnfinnn0  14383  ruclem3  16252  sumodd  16408  bitsinv1lem  16461  sadcaddlem  16477  phiprmpw  16796  iserodd  16856  fldivp1  16918  prmpwdvds  16925  vdwlem6  17007  sylow2alem2  19605  efgs1b  19723  fctop  22959  cctop  22961  ppttop  22962  iccpnfcnv  24912  iccpnfhmeo  24913  iscau2  25248  ovolicc2lem2  25490  mbfeqalem1  25613  limccnp2  25864  radcnv0  26396  psercnlem1  26406  pserdvlem2  26409  logtayl  26639  cxpsqrt  26682  rlimcnp2  26946  amgm  26971  pntpbnd1  27567  pntlem3  27590  nolesgn2o  27653  nogesgn1o  27655  atssma  32326  fsuppcurry1  32672  fsuppcurry2  32673  supxrnemnf  32714  xrge0iifcnv  33907  eulerpartlemf  34347  cusgracyclt3v  35136  arg-ax  36392  pw2f1ocnv  43027  onsupnmax  43218  infordmin  43522  clsk1independent  44036  pm10.57  44362  con5  44514  con3ALT2  44522  xrred  45348  afvco2  47161  islininds2  48374