Theorem con1d 146

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 143	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 36	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 116	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  147  mt3d  149  pm2.24d  152  con3d  153  pm2.61d  181  pm2.8  988  dedlem0b  1060  meredith  1671  ax12ev2  2216  necon3bd  2972  necon1bd  2976  spc2d  3562  sspss  4057  neldif  4089  ssonprc  7787  limsssuc  7847  limom  7879  onfununi  8329  pw2f1olem  9070  domtriord  9112  pssnn  9154  ordtypelem10  9490  rankxpsuc  9855  carden2a  9953  fidomtri2  9981  alephdom  10066  isf32lem12  10349  isfin1-3  10371  isfin7-2  10381  entric  10542  inttsk  10760  zeo  12683  zeo2  12684  xrlttri  13165  xaddf  13251  elfzonelfzo  13800  fzonfzoufzol  13802  elfznelfzo  13804  om2uzf1oi  13991  hashnfinnn0  14399  ruclem3  16290  sumodd  16447  bitsinv1lem  16500  sadcaddlem  16516  phiprmpw  16836  iserodd  16896  fldivp1  16958  prmpwdvds  16965  vdwlem6  17047  sylow2alem2  19689  efgs1b  19807  fctop  23142  cctop  23144  ppttop  23145  iccpnfcnv  25084  iccpnfhmeo  25085  iscau2  25417  ovolicc2lem2  25658  mbfeqalem1  25781  limccnp2  26032  radcnv0  26557  psercnlem1  26566  pserdvlem2  26569  logtayl  26803  cxpsqrt  26846  rlimcnp2  27109  amgm  27133  pntpbnd1  27728  pntlem3  27751  nolesgn2o  27813  nogesgn1o  27815  atssma  32708  fsuppcurry1  33047  fsuppcurry2  33048  supxrnemnf  33091  xrge0iifcnv  34301  eulerpartlemf  34738  onvf1odlem4  35568  cusgracyclt3v  35626  arg-ax  36905  pw2f1ocnv  43744  onsupnmax  43935  infordmin  44238  clsk1independent  44752  pm10.57  45061  con5  45211  con3ALT2  45219  xrred  46060  afvco2  47890  islininds2  49241