Theorem con3d 95

Description: A contraposition deduction.

Hypothesis

Ref	Expression
con3d.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
con3d	⊢ (φ → (¬ χ → ¬ ψ))

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		con3d.1	. 2 ⊢ (φ → (ψ → χ))
2		con3 94	. 2 ⊢ ((ψ → χ) → (¬ χ → ¬ ψ))
3	1, 2	syl 10	1 ⊢ (φ → (¬ χ → ¬ ψ))

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  mtoi 107  mtod 108  nsyld 117  nsyli 121  mth8 123  pm3.48 560  pm5.21nd 684  bibif 685  meredith 928  19.22 1043  a4ime 1164  equs5e 1202  sbn 1235  a12stdy1 1376  a12stdy4 1379  a12studyALT 1383  mo 1397  nelneq 1568  nelneq2 1569  necon3ad 1609  necon3bd 1610  mo2icl 1930  sscon 2182  difrab 2284  disjsn 2453  dtruALT 2764  nsuceq0 3069  limom 3162  relimasn 3441  ndmfv 3761  eqfnfv 3813  dff2 3833  canth 3923  tz7.49 3975  oaord 4197  oalimcl 4210  omord2 4214  omcan 4216  oeord 4231  oecan 4232  nneob 4271  omsmo 4273  erdisj 4302  eceqopreq 4331  domnsym 4482  ensdomtr 4490  domsdomtr 4495  isfinite1 4550  infsdomnn 4551  pssnn 4554  unfi2 4570  unifi2 4574  supmo 4591  kmlem2 4783  alephord 4895  prub 5118  genpnnp 5128  ltaddpr 5160  prlem936 5175  suppsr3 5244  ssxr 5560  prodge0i 5832  nnge1 5957  supxrun 6117  supxrgtmnf 6124  zeo 6234  uzwo4OLD 6245  irrmul 6279  uzwo 6423  uzwoOLD 6424  expord 6633  caucvglem6 7194  elcncf 7297  ivthlem6 7318  infdif 7601  infdif2 7602  lmfexlem1 7982  metelcls 7991  bcthlem7 8031  chnlen0 9392  staddi 10198  stadd3i 10200  strlem1 10202  cvnbtwn 10238  atoml2i 10335  atcvatlem 10337  mdsymlem3 10357  fisub 10605  cnfilca 10609  iintlem1 10653

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain