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  307  aleximi  1757  spc2gv  3291  spc3gv  3293  wfi  5701  soisoi  6563  isomin  6572  riotaclb  6634  extmptsuppeq  7304  mpt2xopynvov0g  7325  boxcutc  7936  sdomel  8092  onsdominel  8094  preleq  8499  cflim2  9070  cfslbn  9074  cofsmo  9076  fincssdom  9130  fin23lem25  9131  fin23lem26  9132  fin1a2s  9221  pwfseqlem4  9469  ltapr  9852  suplem2pr  9860  qsqueeze  12017  ssfzoulel  12546  ssnn0fi  12767  hashbnd  13106  hashclb  13132  hashgt0elex  13172  hashgt12el  13193  hashgt12el2  13194  pc2dvds  15564  infpnlem1  15595  odcl2  17963  ufilmax  21692  ufileu  21704  filufint  21705  hausflim  21766  flimfnfcls  21813  alexsubALTlem3  21834  alexsubALTlem4  21835  reconnlem2  22611  lebnumlem3  22743  rrxmvallem  23168  itg1ge0a  23459  itg2seq  23490  m1lgs  25094  lmieu  25657  axlowdimlem14  25816  usgredg2v  26100  cusgrfilem3  26334  cusgrfi  26335  vtxdgoddnumeven  26430  ex-natded5.13-2  27243  ordtconnlem1  29944  eulerpartlemgh  30414  bnj23  30758  frind  31714  nosepon  31792  nn0prpw  32293  meran1  32385  finxpreclem6  33204  wl-spae  33277  poimirlem32  33412  heiborlem1  33581  riotaclbgBAD  34059  reclt0  39427  limclr  39687  eu2ndop1stv  40965  mndpsuppss  41917
 Copyright terms: Public domain W3C validator