Theorem con1d 142

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 139	. . 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:  mt3d  143  con1  146  pm2.24d  149  con3d  150  pm2.61d  172  pm2.8  958  dedlem0b  1028  meredith  1685  axc16nf  2236  necon3bd  2983  necon1bd  2987  sspss  3928  neldif  3958  ssonprc  7270  limsssuc  7328  limom  7358  onfununi  7721  pw2f1olem  8352  domtriord  8394  pssnn  8466  ordtypelem10  8721  rankxpsuc  9042  carden2a  9125  fidomtri2  9153  alephdom  9237  isf32lem12  9521  isfin1-3  9543  isfin7-2  9553  entric  9714  inttsk  9931  zeo  11815  zeo2  11816  xrlttri  12282  xaddf  12367  elfzonelfzo  12889  fzonfzoufzol  12890  elfznelfzo  12892  om2uzf1oi  13071  hashnfinnn0  13467  ruclem3  15366  sumodd  15518  bitsinv1lem  15569  sadcaddlem  15585  phiprmpw  15885  iserodd  15944  fldivp1  16005  prmpwdvds  16012  vdwlem6  16094  sylow2alem2  18417  efgs1b  18533  fctop  21216  cctop  21218  ppttop  21219  iccpnfcnv  23151  iccpnfhmeo  23152  iscau2  23483  ovolicc2lem2  23722  mbfeqalem1  23845  limccnp2  24093  radcnv0  24607  psercnlem1  24616  pserdvlem2  24619  logtayl  24843  cxpsqrt  24886  leibpilem1OLD  25119  rlimcnp2  25145  amgm  25169  pntpbnd1  25727  pntlem3  25750  atssma  29809  spc2d  29885  supxrnemnf  30099  xrge0iifcnv  30577  eulerpartlemf  31030  nolesgn2o  32413  arg-ax  32998  pw2f1ocnv  38563  clsk1independent  39300  pm10.57  39526  con5  39682  con3ALT2  39690  xrred  40489  afvco2  42217  islininds2  43288