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  3107  spc2gv  3558  spc3gv  3562  frpoind  6363  soisoi  7359  isomin  7368  riotaclb  7441  extmptsuppeq  8233  mpoxopynvov0g  8259  fsetcdmex  8913  boxcutc  8997  sdomel  9171  onsdominel  9173  preleqALT  9645  frind  9781  cflim2  10368  cfslbn  10372  cofsmo  10374  fincssdom  10428  fin23lem25  10429  fin23lem26  10430  fin1a2s  10519  pwfseqlem4  10774  ltapr  11157  suplem2pr  11165  qsqueeze  13358  ssfzoulel  13922  ssnn0fi  14155  hashbnd  14507  hashclb  14529  hashgt0elex  14572  hashgt12el  14594  hashgt12el2  14595  2mulprm  16897  pc2dvds  17086  infpnlem1  17117  mndpsuppss  18988  odcl2  19809  ufilmax  24256  ufileu  24268  filufint  24269  hausflim  24330  flimfnfcls  24377  alexsubALTlem3  24398  alexsubALTlem4  24399  reconnlem2  25177  lebnumlem3  25314  rrxmvallem  25755  itg1ge0a  26062  itg2seq  26093  m1lgs  27745  nosepon  28052  leadds1im  28403  leadds1  28405  oncutlt  28680  onnolt  28682  bdaypw2n0bndlem  28879  lmieu  29319  axlowdimlem14  29563  usgredg2v  29838  cusgrfilem3  30068  cusgrfi  30069  vtxdgoddnumeven  30164  clwwlknon1sn  30721  ex-natded5.13-2  31047  diffib  33189  ordtconnlem1  34626  eulerpartlemgh  35080  bnj23  35419  onprcf1acwevdlem1  36045  nn0prpw  37289  meran1  37377  mh-regprimbi  37511  finxpreclem6  38511  wl-spae  38645  poimirlem32  38762  heiborlem1  38937  riotaclbgBAD  40203  primrootspoweq0  43348  aks6d1c2p2  43361  hashscontpow  43364  aks6d1c5lem1  43378  aks6d1c6lem3  43414  ioin9i8  43451  onsupmaxb  44433  onsupsucismax  44473  tfsconcat0b  44540  relpmin  46137  reclt0  46607  limclr  46870  eu2ndop1stv  48400  requad01  48924  line2ylem  50068  line2xlem  50070