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 ⊢ (𝜑 → (𝜒 → 𝜓))

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:  mt4d  118  pm2.21d  122  con2d  135  con1d  146  impcon4bid  230  con4bid  320  aleximi  1862  rexim  3106  spc2gv  3560  spc3gv  3564  frpoind  6345  soisoi  7328  isomin  7337  riotaclb  7410  extmptsuppeq  8185  mpoxopynvov0g  8211  fsetcdmex  8861  boxcutc  8940  sdomel  9113  onsdominel  9115  preleqALT  9587  frind  9723  cflim2  10248  cfslbn  10252  cofsmo  10254  fincssdom  10308  fin23lem25  10309  fin23lem26  10310  fin1a2s  10399  pwfseqlem4  10648  ltapr  11031  suplem2pr  11039  qsqueeze  13228  ssfzoulel  13791  ssnn0fi  14023  hashbnd  14374  hashclb  14396  hashgt0elex  14439  hashgt12el  14461  hashgt12el2  14462  2mulprm  16752  pc2dvds  16940  infpnlem1  16971  mndpsuppss  18824  odcl2  19636  ufilmax  24045  ufileu  24057  filufint  24058  hausflim  24119  flimfnfcls  24166  alexsubALTlem3  24187  alexsubALTlem4  24188  reconnlem2  24966  lebnumlem3  25103  rrxmvallem  25544  itg1ge0a  25851  itg2seq  25882  m1lgs  27530  nosepon  27807  leadds1im  28158  leadds1  28160  oncutlt  28435  onnolt  28437  bdaypw2n0bndlem  28634  lmieu  29071  axlowdimlem14  29283  usgredg2v  29555  cusgrfilem3  29785  cusgrfi  29786  vtxdgoddnumeven  29881  clwwlknon1sn  30429  ex-natded5.13-2  30745  diffib  32845  ordtconnlem1  34292  eulerpartlemgh  34746  bnj23  35085  nn0prpw  36812  meran1  36900  mh-regprimbi  37034  finxpreclem6  38020  wl-spae  38154  poimirlem32  38281  heiborlem1  38440  riotaclbgBAD  39706  primrootspoweq0  42851  aks6d1c2p2  42864  hashscontpow  42867  aks6d1c5lem1  42881  aks6d1c6lem3  42917  ioin9i8  42954  onsupmaxb  43946  onsupsucismax  43986  tfsconcat0b  44053  relpmin  45641  reclt0  46086  limclr  46349  eu2ndop1stv  47839  requad01  48363  line2ylem  49508  line2xlem  49510