Theorem con1d 139

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 136	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 35	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 114	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  140  con1  143  pm2.24d  147  con3d  148  pm2.61d  170  pm2.8  894  dedlem0b  1000  meredith  1563  axc11nlemOLD2  1985  axc16nf  2133  hbntOLD  2141  axc11nlemOLD  2157  axc11nlemALT  2305  necon3bd  2804  necon1bd  2808  sspss  3684  neldif  3713  ssonprc  6939  limsssuc  6997  limom  7027  onfununi  7383  pw2f1olem  8008  domtriord  8050  pssnn  8122  ordtypelem10  8376  rankxpsuc  8689  carden2a  8736  fidomtri2  8764  alephdom  8848  isf32lem12  9130  isfin1-3  9152  isfin7-2  9162  entric  9323  inttsk  9540  zeo  11407  zeo2  11408  xrlttri  11916  xaddf  11998  elfzonelfzo  12511  fzonfzoufzol  12512  elfznelfzo  12514  om2uzf1oi  12692  hashnfinnn0  13092  ruclem3  14887  sumodd  15035  bitsinv1lem  15087  sadcaddlem  15103  phiprmpw  15405  iserodd  15464  fldivp1  15525  prmpwdvds  15532  vdwlem6  15614  sylow2alem2  17954  efgs1b  18070  fctop  20718  cctop  20720  ppttop  20721  iccpnfcnv  22651  iccpnfhmeo  22652  iscau2  22983  ovolicc2lem2  23193  mbfeqalem  23315  limccnp2  23562  radcnv0  24074  psercnlem1  24083  pserdvlem2  24086  logtayl  24306  cxpsqrt  24349  leibpilem1  24567  rlimcnp2  24593  amgm  24617  pntpbnd1  25175  pntlem3  25198  atssma  29083  spc2d  29159  supxrnemnf  29375  xrge0iifcnv  29758  eulerpartlemf  30210  arg-ax  32054  pw2f1ocnv  37081  clsk1independent  37823  pm10.57  38049  con5  38207  con3ALT2  38215  xrred  39042  afvco2  40557  islininds2  41558