MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con4d Structured version   Visualization version   GIF version

Theorem con4d 113
Description: Deduction associated with con4 111. (Contributed by NM, 26-Mar-1995.)
Hypothesis
Ref Expression
con4d.1 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
Assertion
Ref Expression
con4d (𝜑 → (𝜒𝜓))

Proof of Theorem con4d
StepHypRef Expression
1 con4d.1 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
2 con4 111 . 2 ((¬ 𝜓 → ¬ 𝜒) → (𝜒𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
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:  pm2.21d  117  pm2.18  121  con2d  128  con1d  138  mt4d  151  impcon4bid  216  con4bid  306  aleximi  1749  spc2gv  3269  spc3gv  3271  wfi  5630  soisoi  6478  isomin  6487  riotaclb  6548  extmptsuppeq  7206  mpt2xopynvov0g  7227  boxcutc  7837  sdomel  7992  onsdominel  7994  preleq  8397  cflim2  8968  cfslbn  8972  cofsmo  8974  fincssdom  9028  fin23lem25  9029  fin23lem26  9030  fin1a2s  9119  pwfseqlem4  9363  ltapr  9746  suplem2pr  9754  qsqueeze  11906  ssfzoulel  12428  ssnn0fi  12646  hashbnd  12985  hashclb  13011  hashgt0elex  13050  hashgt12el  13070  hashgt12el2  13071  pc2dvds  15421  infpnlem1  15452  odcl2  17805  ufilmax  21521  ufileu  21533  filufint  21534  hausflim  21595  flimfnfcls  21642  alexsubALTlem3  21663  alexsubALTlem4  21664  reconnlem2  22438  lebnumlem3  22570  rrxmvallem  22995  itg1ge0a  23284  itg2seq  23315  m1lgs  24913  lmieu  25476  axlowdimlem14  25635  usgraidx2v  25922  cusgrafilem3  26009  cusgrafi  26010  usgrcyclnl1  26168  ex-natded5.13-2  26665  ordtconlem1  29298  eulerpartlemgh  29767  bnj23  30038  frind  30984  nosepon  31066  nn0prpw  31488  meran1  31580  finxpreclem6  32409  wl-spae  32485  poimirlem32  32611  heiborlem1  32780  riotaclbgBAD  33258  reclt0  38555  limclr  38722  eu2ndop1stv  39851  usgredg2v  40454  cusgrfilem3  40673  cusgrfi  40674  mndpsuppss  41946
  Copyright terms: Public domain W3C validator