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  1641  ax12ev2  2181  necon3bd  2947  necon1bd  2951  spc2d  3586  sspss  4082  neldif  4114  ssonprc  7786  limsssuc  7850  limom  7882  onfununi  8360  pw2f1olem  9095  domtriord  9142  pssnn  9187  ordtypelem10  9546  rankxpsuc  9901  carden2a  9985  fidomtri2  10013  alephdom  10100  isf32lem12  10383  isfin1-3  10405  isfin7-2  10415  entric  10576  inttsk  10793  zeo  12684  zeo2  12685  xrlttri  13160  xaddf  13245  elfzonelfzo  13790  fzonfzoufzol  13791  elfznelfzo  13793  om2uzf1oi  13976  hashnfinnn0  14384  ruclem3  16256  sumodd  16412  bitsinv1lem  16465  sadcaddlem  16481  phiprmpw  16800  iserodd  16860  fldivp1  16922  prmpwdvds  16929  vdwlem6  17011  sylow2alem2  19604  efgs1b  19722  fctop  22947  cctop  22949  ppttop  22950  iccpnfcnv  24898  iccpnfhmeo  24899  iscau2  25234  ovolicc2lem2  25476  mbfeqalem1  25599  limccnp2  25850  radcnv0  26382  psercnlem1  26392  pserdvlem2  26395  logtayl  26626  cxpsqrt  26669  rlimcnp2  26933  amgm  26958  pntpbnd1  27554  pntlem3  27577  nolesgn2o  27640  nogesgn1o  27642  atssma  32364  fsuppcurry1  32707  fsuppcurry2  32708  supxrnemnf  32750  xrge0iifcnv  33969  eulerpartlemf  34407  cusgracyclt3v  35183  arg-ax  36439  pw2f1ocnv  43036  onsupnmax  43227  infordmin  43531  clsk1independent  44045  pm10.57  44370  con5  44522  con3ALT2  44530  xrred  45372  afvco2  47185  islininds2  48440