Theorem con4d 116

Description: Deduction associated with con4 114. (Contributed by NM, 26-Mar-1995.)

Hypothesis

Ref	Expression
con4d.1	⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
con4d	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem con4d

Step	Hyp	Ref	Expression
1		con4d.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
2		con4 114	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜒) → (𝜒 → 𝜓))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt4d  118  pm2.21d  122  con2d  135  con1d  146  impcon4bid  230  con4bid  320  aleximi  1865  rexim  3109  spc2gv  3562  spc3gv  3566  frpoind  6350  soisoi  7337  isomin  7346  riotaclb  7421  extmptsuppeq  8193  mpoxopynvov0g  8219  fsetcdmex  8869  boxcutc  8948  sdomel  9122  onsdominel  9124  preleqALT  9596  frind  9732  cflim2  10265  cfslbn  10269  cofsmo  10271  fincssdom  10325  fin23lem25  10326  fin23lem26  10327  fin1a2s  10416  pwfseqlem4  10665  ltapr  11048  suplem2pr  11056  qsqueeze  13245  ssfzoulel  13808  ssnn0fi  14041  hashbnd  14392  hashclb  14414  hashgt0elex  14457  hashgt12el  14479  hashgt12el2  14480  2mulprm  16776  pc2dvds  16964  infpnlem1  16995  mndpsuppss  18854  odcl2  19666  ufilmax  24101  ufileu  24113  filufint  24114  hausflim  24175  flimfnfcls  24222  alexsubALTlem3  24243  alexsubALTlem4  24244  reconnlem2  25022  lebnumlem3  25159  rrxmvallem  25600  itg1ge0a  25907  itg2seq  25938  m1lgs  27589  nosepon  27866  leadds1im  28217  leadds1  28219  oncutlt  28494  onnolt  28496  bdaypw2n0bndlem  28693  lmieu  29130  axlowdimlem14  29342  usgredg2v  29614  cusgrfilem3  29844  cusgrfi  29845  vtxdgoddnumeven  29940  clwwlknon1sn  30488  ex-natded5.13-2  30804  diffib  32904  ordtconnlem1  34345  eulerpartlemgh  34800  bnj23  35139  nn0prpw  36875  meran1  36963  mh-regprimbi  37097  finxpreclem6  38083  wl-spae  38217  poimirlem32  38344  heiborlem1  38503  riotaclbgBAD  39769  primrootspoweq0  42914  aks6d1c2p2  42927  hashscontpow  42930  aks6d1c5lem1  42944  aks6d1c6lem3  42980  ioin9i8  43017  onsupmaxb  44007  onsupsucismax  44047  tfsconcat0b  44114  relpmin  45702  reclt0  46147  limclr  46410  eu2ndop1stv  47903  requad01  48427  line2ylem  49572  line2xlem  49574