Theorem con1d 141

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 138	. . 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:  mt3d  142  con1  145  pm2.24d  148  con3d  149  pm2.61d  171  pm2.8  947  dedlem0b  1029  meredith  1714  axc16nf  2302  hbntOLD  2310  necon3bd  2957  necon1bd  2961  sspss  3857  neldif  3887  ssonprc  7140  limsssuc  7198  limom  7228  onfununi  7592  pw2f1olem  8221  domtriord  8263  pssnn  8335  ordtypelem10  8589  rankxpsuc  8910  carden2a  8993  fidomtri2  9021  alephdom  9105  isf32lem12  9389  isfin1-3  9411  isfin7-2  9421  entric  9582  inttsk  9799  zeo  11666  zeo2  11667  xrlttri  12178  xaddf  12261  elfzonelfzo  12779  fzonfzoufzol  12780  elfznelfzo  12782  om2uzf1oi  12961  hashnfinnn0  13355  ruclem3  15169  sumodd  15320  bitsinv1lem  15372  sadcaddlem  15388  phiprmpw  15689  iserodd  15748  fldivp1  15809  prmpwdvds  15816  vdwlem6  15898  sylow2alem2  18241  efgs1b  18357  fctop  21030  cctop  21032  ppttop  21033  iccpnfcnv  22964  iccpnfhmeo  22965  iscau2  23295  ovolicc2lem2  23507  mbfeqalem  23630  limccnp2  23877  radcnv0  24391  psercnlem1  24400  pserdvlem2  24403  logtayl  24628  cxpsqrt  24671  leibpilem1  24889  rlimcnp2  24915  amgm  24939  pntpbnd1  25497  pntlem3  25520  atssma  29578  spc2d  29654  supxrnemnf  29875  xrge0iifcnv  30320  eulerpartlemf  30773  nolesgn2o  32162  arg-ax  32753  pw2f1ocnv  38131  clsk1independent  38871  pm10.57  39097  con5  39254  con3ALT2  39262  xrred  40098  afvco2  41777  islininds2  42802