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  972  dedlem0b  1044  meredith  1644  necon3bd  2955  necon1bd  2959  spc2d  3593  sspss  4100  neldif  4130  ssonprc  7775  limsssuc  7839  limom  7871  onfununi  8341  pw2f1olem  9076  domtriord  9123  pssnn  9168  pssnnOLD  9265  ordtypelem10  9522  rankxpsuc  9877  carden2a  9961  fidomtri2  9989  alephdom  10076  isf32lem12  10359  isfin1-3  10381  isfin7-2  10391  entric  10552  inttsk  10769  zeo  12648  zeo2  12649  xrlttri  13118  xaddf  13203  elfzonelfzo  13734  fzonfzoufzol  13735  elfznelfzo  13737  om2uzf1oi  13918  hashnfinnn0  14321  ruclem3  16176  sumodd  16331  bitsinv1lem  16382  sadcaddlem  16398  phiprmpw  16709  iserodd  16768  fldivp1  16830  prmpwdvds  16837  vdwlem6  16919  sylow2alem2  19486  efgs1b  19604  fctop  22507  cctop  22509  ppttop  22510  iccpnfcnv  24460  iccpnfhmeo  24461  iscau2  24794  ovolicc2lem2  25035  mbfeqalem1  25158  limccnp2  25409  radcnv0  25928  psercnlem1  25937  pserdvlem2  25940  logtayl  26168  cxpsqrt  26211  rlimcnp2  26471  amgm  26495  pntpbnd1  27089  pntlem3  27112  nolesgn2o  27174  nogesgn1o  27176  atssma  31631  fsuppcurry1  31950  fsuppcurry2  31951  supxrnemnf  31981  xrge0iifcnv  32913  eulerpartlemf  33369  cusgracyclt3v  34147  arg-ax  35301  pw2f1ocnv  41776  onsupnmax  41977  infordmin  42283  clsk1independent  42797  pm10.57  43130  con5  43283  con3ALT2  43291  xrred  44075  afvco2  45884  islininds2  47165