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  7272  limsssuc  7330  limom  7360  onfununi  7723  pw2f1olem  8354  domtriord  8396  pssnn  8468  ordtypelem10  8723  rankxpsuc  9044  carden2a  9127  fidomtri2  9155  alephdom  9239  isf32lem12  9523  isfin1-3  9545  isfin7-2  9555  entric  9716  inttsk  9933  zeo  11820  zeo2  11821  xrlttri  12287  xaddf  12372  elfzonelfzo  12894  fzonfzoufzol  12895  elfznelfzo  12897  om2uzf1oi  13076  hashnfinnn0  13473  ruclem3  15375  sumodd  15528  bitsinv1lem  15579  sadcaddlem  15595  phiprmpw  15896  iserodd  15955  fldivp1  16016  prmpwdvds  16023  vdwlem6  16105  sylow2alem2  18428  efgs1b  18544  fctop  21227  cctop  21229  ppttop  21230  iccpnfcnv  23162  iccpnfhmeo  23163  iscau2  23494  ovolicc2lem2  23733  mbfeqalem1  23856  limccnp2  24104  radcnv0  24618  psercnlem1  24627  pserdvlem2  24630  logtayl  24854  cxpsqrt  24897  leibpilem1OLD  25130  rlimcnp2  25156  amgm  25180  pntpbnd1  25744  pntlem3  25767  atssma  29826  spc2d  29902  supxrnemnf  30113  xrge0iifcnv  30585  eulerpartlemf  31038  nolesgn2o  32421  arg-ax  33006  pw2f1ocnv  38577  clsk1independent  39314  pm10.57  39540  con5  39696  con3ALT2  39704  xrred  40503  afvco2  42231  islininds2  43302