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

Theorem con4d 112
Description: Deduction associated with con4 110. (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 110 . 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  116  pm2.18  120  con2d  127  con1d  137  mt4d  150  impcon4bid  215  con4bid  305  aleximi  1748  spc2gv  3265  spc3gv  3267  wfi  5613  soisoi  6453  isomin  6462  riotaclb  6523  extmptsuppeq  7180  mpt2xopynvov0g  7201  boxcutc  7811  sdomel  7966  onsdominel  7968  preleq  8371  cflim2  8942  cfslbn  8946  cofsmo  8948  fincssdom  9002  fin23lem25  9003  fin23lem26  9004  fin1a2s  9093  pwfseqlem4  9337  ltapr  9720  suplem2pr  9728  qsqueeze  11862  ssfzoulel  12380  ssnn0fi  12598  hashbnd  12937  hashclb  12960  hashgt0elex  12999  hashgt12el  13019  hashgt12el2  13020  pc2dvds  15364  infpnlem1  15395  odcl2  17748  ufilmax  21460  ufileu  21472  filufint  21473  hausflim  21534  flimfnfcls  21581  alexsubALTlem3  21602  alexsubALTlem4  21603  reconnlem2  22367  lebnumlem3  22498  rrxmvallem  22909  itg1ge0a  23198  itg2seq  23229  m1lgs  24827  lmieu  25391  axlowdimlem14  25550  usgraidx2v  25685  cusgrafilem3  25772  cusgrafi  25773  usgrcyclnl1  25931  ex-natded5.13-2  26428  ordtconlem1  29101  eulerpartlemgh  29570  bnj23  29841  frind  30787  nosepon  30869  nn0prpw  31291  meran1  31383  finxpreclem6  32209  wl-spae  32285  poimirlem32  32411  heiborlem1  32580  riotaclbgBAD  33058  reclt0  38356  limclr  38523  eu2ndop1stv  39652  usgredg2v  40453  cusgrfilem3  40672  cusgrfi  40673  mndpsuppss  41945
  Copyright terms: Public domain W3C validator