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  1638  ax12ev2  2178  necon3bd  2952  necon1bd  2956  spc2d  3602  sspss  4112  neldif  4144  ssonprc  7807  limsssuc  7871  limom  7903  onfununi  8380  pw2f1olem  9115  domtriord  9162  pssnn  9207  ordtypelem10  9565  rankxpsuc  9920  carden2a  10004  fidomtri2  10032  alephdom  10119  isf32lem12  10402  isfin1-3  10424  isfin7-2  10434  entric  10595  inttsk  10812  zeo  12702  zeo2  12703  xrlttri  13178  xaddf  13263  elfzonelfzo  13805  fzonfzoufzol  13806  elfznelfzo  13808  om2uzf1oi  13991  hashnfinnn0  14397  ruclem3  16266  sumodd  16422  bitsinv1lem  16475  sadcaddlem  16491  phiprmpw  16810  iserodd  16869  fldivp1  16931  prmpwdvds  16938  vdwlem6  17020  sylow2alem2  19651  efgs1b  19769  fctop  23027  cctop  23029  ppttop  23030  iccpnfcnv  24989  iccpnfhmeo  24990  iscau2  25325  ovolicc2lem2  25567  mbfeqalem1  25690  limccnp2  25942  radcnv0  26474  psercnlem1  26484  pserdvlem2  26487  logtayl  26717  cxpsqrt  26760  rlimcnp2  27024  amgm  27049  pntpbnd1  27645  pntlem3  27668  nolesgn2o  27731  nogesgn1o  27733  atssma  32407  fsuppcurry1  32743  fsuppcurry2  32744  supxrnemnf  32779  xrge0iifcnv  33894  eulerpartlemf  34352  cusgracyclt3v  35141  arg-ax  36399  pw2f1ocnv  43026  onsupnmax  43217  infordmin  43522  clsk1independent  44036  pm10.57  44367  con5  44520  con3ALT2  44528  xrred  45315  afvco2  47126  islininds2  48330