Theorem con1d 147

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 144	. . 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  148  mt3d  150  pm2.24d  154  con3d  155  pm2.61d  181  pm2.8  969  dedlem0b  1039  meredith  1638  necon3bd  3030  necon1bd  3034  spc2d  3602  sspss  4075  neldif  4105  ssonprc  7501  limsssuc  7559  limom  7589  onfununi  7972  pw2f1olem  8615  domtriord  8657  pssnn  8730  ordtypelem10  8985  rankxpsuc  9305  carden2a  9389  fidomtri2  9417  alephdom  9501  isf32lem12  9780  isfin1-3  9802  isfin7-2  9812  entric  9973  inttsk  10190  zeo  12062  zeo2  12063  xrlttri  12526  xaddf  12611  elfzonelfzo  13133  fzonfzoufzol  13134  elfznelfzo  13136  om2uzf1oi  13315  hashnfinnn0  13716  ruclem3  15580  sumodd  15733  bitsinv1lem  15784  sadcaddlem  15800  phiprmpw  16107  iserodd  16166  fldivp1  16227  prmpwdvds  16234  vdwlem6  16316  sylow2alem2  18737  efgs1b  18856  fctop  21606  cctop  21608  ppttop  21609  iccpnfcnv  23542  iccpnfhmeo  23543  iscau2  23874  ovolicc2lem2  24113  mbfeqalem1  24236  limccnp2  24484  radcnv0  24998  psercnlem1  25007  pserdvlem2  25010  logtayl  25237  cxpsqrt  25280  rlimcnp2  25538  amgm  25562  pntpbnd1  26156  pntlem3  26179  atssma  30149  fsuppcurry1  30455  fsuppcurry2  30456  supxrnemnf  30487  xrge0iifcnv  31171  eulerpartlemf  31623  cusgracyclt3v  32398  nolesgn2o  33173  arg-ax  33759  pw2f1ocnv  39627  infordmin  39892  clsk1independent  40389  pm10.57  40696  con5  40849  con3ALT2  40857  xrred  41626  afvco2  43369  islininds2  44533