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

Theorem con4d 114
 Description: Deduction associated with con4 112. (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 112 . 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  118  pm2.18  122  con2d  129  con1d  139  mt4d  152  impcon4bid  217  con4bid  306  aleximi  1799  spc2gv  3327  spc3gv  3329  wfi  5751  soisoi  6618  isomin  6627  riotaclb  6689  extmptsuppeq  7364  mpt2xopynvov0g  7385  boxcutc  7993  sdomel  8148  onsdominel  8150  preleq  8552  cflim2  9123  cfslbn  9127  cofsmo  9129  fincssdom  9183  fin23lem25  9184  fin23lem26  9185  fin1a2s  9274  pwfseqlem4  9522  ltapr  9905  suplem2pr  9913  qsqueeze  12070  ssfzoulel  12602  ssnn0fi  12824  hashbnd  13163  hashclb  13187  hashgt0elex  13227  hashgt12el  13248  hashgt12el2  13249  pc2dvds  15630  infpnlem1  15661  odcl2  18028  ufilmax  21758  ufileu  21770  filufint  21771  hausflim  21832  flimfnfcls  21879  alexsubALTlem3  21900  alexsubALTlem4  21901  reconnlem2  22677  lebnumlem3  22809  rrxmvallem  23233  itg1ge0a  23523  itg2seq  23554  m1lgs  25158  lmieu  25721  axlowdimlem14  25880  usgredg2v  26164  cusgrfilem3  26409  cusgrfi  26410  vtxdgoddnumeven  26505  clwwlknon1sn  27075  ex-natded5.13-2  27403  ordtconnlem1  30098  eulerpartlemgh  30568  bnj23  30912  frpoind  31865  frind  31868  nosepon  31943  nn0prpw  32443  meran1  32535  finxpreclem6  33363  wl-spae  33436  poimirlem32  33571  heiborlem1  33740  riotaclbgBAD  34558  reclt0  39927  limclr  40205  eu2ndop1stv  41523  mndpsuppss  42477
 Copyright terms: Public domain W3C validator