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  182  pm2.8  970  dedlem0b  1040  meredith  1643  necon3bd  3001  necon1bd  3005  spc2d  3551  sspss  4027  neldif  4057  ssonprc  7487  limsssuc  7545  limom  7575  onfununi  7961  pw2f1olem  8604  domtriord  8647  pssnn  8720  ordtypelem10  8975  rankxpsuc  9295  carden2a  9379  fidomtri2  9407  alephdom  9492  isf32lem12  9775  isfin1-3  9797  isfin7-2  9807  entric  9968  inttsk  10185  zeo  12056  zeo2  12057  xrlttri  12520  xaddf  12605  elfzonelfzo  13134  fzonfzoufzol  13135  elfznelfzo  13137  om2uzf1oi  13316  hashnfinnn0  13718  ruclem3  15578  sumodd  15729  bitsinv1lem  15780  sadcaddlem  15796  phiprmpw  16103  iserodd  16162  fldivp1  16223  prmpwdvds  16230  vdwlem6  16312  sylow2alem2  18735  efgs1b  18854  fctop  21609  cctop  21611  ppttop  21612  iccpnfcnv  23549  iccpnfhmeo  23550  iscau2  23881  ovolicc2lem2  24122  mbfeqalem1  24245  limccnp2  24495  radcnv0  25011  psercnlem1  25020  pserdvlem2  25023  logtayl  25251  cxpsqrt  25294  rlimcnp2  25552  amgm  25576  pntpbnd1  26170  pntlem3  26193  atssma  30161  fsuppcurry1  30487  fsuppcurry2  30488  supxrnemnf  30519  xrge0iifcnv  31286  eulerpartlemf  31738  cusgracyclt3v  32516  nolesgn2o  33291  arg-ax  33877  pw2f1ocnv  39978  infordmin  40240  clsk1independent  40749  pm10.57  41075  con5  41228  con3ALT2  41236  xrred  41997  afvco2  43732  islininds2  44893