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

Theorem con4d 115
Description: Deduction associated with con4 113. (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 113 . 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:  mt4d  117  pm2.21d  121  pm2.18OLD  129  con2d  136  con1d  147  impcon4bid  230  con4bid  320  norassOLD  1535  aleximi  1833  spc2gv  3549  spc3gv  3553  wfi  6149  soisoi  7060  isomin  7069  riotaclb  7134  extmptsuppeq  7837  mpoxopynvov0g  7863  boxcutc  8488  sdomel  8648  onsdominel  8650  preleqALT  9064  cflim2  9674  cfslbn  9678  cofsmo  9680  fincssdom  9734  fin23lem25  9735  fin23lem26  9736  fin1a2s  9825  pwfseqlem4  10073  ltapr  10456  suplem2pr  10464  qsqueeze  12582  ssfzoulel  13126  ssnn0fi  13348  hashbnd  13692  hashclb  13715  hashgt0elex  13758  hashgt12el  13779  hashgt12el2  13780  2mulprm  16027  pc2dvds  16205  infpnlem1  16236  odcl2  18684  ufilmax  22512  ufileu  22524  filufint  22525  hausflim  22586  flimfnfcls  22633  alexsubALTlem3  22654  alexsubALTlem4  22655  reconnlem2  23432  lebnumlem3  23568  rrxmvallem  24008  itg1ge0a  24315  itg2seq  24346  m1lgs  25972  lmieu  26578  axlowdimlem14  26749  usgredg2v  27017  cusgrfilem3  27247  cusgrfi  27248  vtxdgoddnumeven  27343  clwwlknon1sn  27885  ex-natded5.13-2  28201  diffib  30293  ordtconnlem1  31277  eulerpartlemgh  31746  bnj23  32098  frpoind  33193  frind  33198  nosepon  33285  nn0prpw  33784  meran1  33872  finxpreclem6  34813  wl-spae  34926  poimirlem32  35089  heiborlem1  35249  riotaclbgBAD  36250  ioin9i8  39387  reclt0  42025  limclr  42295  eu2ndop1stv  43679  requad01  44137  mndpsuppss  44771  line2ylem  45163  line2xlem  45165
  Copyright terms: Public domain W3C validator