Theorem con1d 131

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 128	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 34	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 110	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  132  con1  135  pm2.24d  141  con3d  142  pm2.61d  165  pm2.8  881  dedlem0b  982  meredith  1554  axc11nlemOLD2  1935  hbnt  2029  axc11nlemOLD  2074  axc11nlemALT  2190  necon3bd  2691  necon1bd  2695  sspss  3554  neldif  3583  ssonprc  6696  limsssuc  6754  limom  6784  onfununi  7137  pw2f1olem  7760  domtriord  7802  pssnn  7874  ordtypelem10  8125  rankxpsuc  8438  carden2a  8485  fidomtri2  8513  alephdom  8597  isf32lem12  8879  isfin1-3  8901  isfin7-2  8911  entric  9067  inttsk  9284  zeo  11111  zeo2  11112  xrlttri  11529  xaddf  11610  elfzonelfzo  12117  fzonfzoufzol  12118  elfznelfzo  12120  om2uzf1oi  12280  hashnfinnn0  12660  ruclem3  14445  bitsinv1lem  14577  sadcaddlem  14593  phiprmpw  14886  iserodd  14947  fldivp1  15004  prmpwdvds  15010  vdwlem6  15098  sylow2alem2  17431  efgs1b  17547  fctop  20176  cctop  20178  ppttop  20179  iccpnfcnv  22130  iccpnfhmeo  22131  iscau2  22406  ovolicc2lem2  22630  mbfeqalem  22759  limccnp2  23008  radcnv0  23532  psercnlem1  23541  pserdvlem2  23544  logtayl  23766  cxpsqrt  23809  leibpilem1  24027  rlimcnp2  24053  amgm  24077  pntpbnd1  24585  pntlem3  24608  atssma  28194  spc2d  28270  supxrnemnf  28510  xrge0iifcnv  28894  eulerpartlemf  29357  arg-ax  31225  bj-axc11nlemv  31534  pw2f1ocnv  36132  pm10.57  37077  con5  37235  con3ALT2  37243  xrred  37964  afvco2  39198  islininds2  41467