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  931  dedlem0b  1031  meredith  1703  axc16nf  2272  hbntOLD  2280  necon3bd  2934  necon1bd  2938  sspss  3836  neldif  3866  ssonprc  7145  limsssuc  7203  limom  7233  onfununi  7595  pw2f1olem  8217  domtriord  8259  pssnn  8331  ordtypelem10  8585  rankxpsuc  8906  carden2a  8953  fidomtri2  8981  alephdom  9065  isf32lem12  9349  isfin1-3  9371  isfin7-2  9381  entric  9542  inttsk  9759  zeo  11626  zeo2  11627  xrlttri  12136  xaddf  12219  elfzonelfzo  12735  fzonfzoufzol  12736  elfznelfzo  12738  om2uzf1oi  12917  hashnfinnn0  13315  ruclem3  15132  sumodd  15284  bitsinv1lem  15336  sadcaddlem  15352  phiprmpw  15654  iserodd  15713  fldivp1  15774  prmpwdvds  15781  vdwlem6  15863  sylow2alem2  18204  efgs1b  18320  fctop  20981  cctop  20983  ppttop  20984  iccpnfcnv  22915  iccpnfhmeo  22916  iscau2  23246  ovolicc2lem2  23457  mbfeqalem  23579  limccnp2  23826  radcnv0  24340  psercnlem1  24349  pserdvlem2  24352  logtayl  24576  cxpsqrt  24619  leibpilem1  24837  rlimcnp2  24863  amgm  24887  pntpbnd1  25445  pntlem3  25468  atssma  29517  spc2d  29593  supxrnemnf  29814  xrge0iifcnv  30259  eulerpartlemf  30712  nolesgn2o  32101  arg-ax  32692  pw2f1ocnv  38075  clsk1independent  38815  pm10.57  39041  con5  39199  con3ALT2  39207  xrred  40048  afvco2  41731  islininds2  42752