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  con2d  134  con1d  145  impcon4bid  226  con4bid  317  aleximi  1835  rexim  3089  spc2gv  3558  spc3gv  3562  frpoind  6295  wfiOLD  6304  soisoi  7270  isomin  7279  riotaclb  7350  extmptsuppeq  8112  mpoxopynvov0g  8138  fsetcdmex  8760  boxcutc  8838  sdomel  9027  onsdominel  9029  preleqALT  9512  frind  9645  cflim2  10158  cfslbn  10162  cofsmo  10164  fincssdom  10218  fin23lem25  10219  fin23lem26  10220  fin1a2s  10309  pwfseqlem4  10557  ltapr  10940  suplem2pr  10948  qsqueeze  13075  ssfzoulel  13621  ssnn0fi  13845  hashbnd  14190  hashclb  14212  hashgt0elex  14255  hashgt12el  14276  hashgt12el2  14277  2mulprm  16529  pc2dvds  16711  infpnlem1  16742  odcl2  19306  ufilmax  23210  ufileu  23222  filufint  23223  hausflim  23284  flimfnfcls  23331  alexsubALTlem3  23352  alexsubALTlem4  23353  reconnlem2  24142  lebnumlem3  24278  rrxmvallem  24720  itg1ge0a  25028  itg2seq  25059  m1lgs  26688  nosepon  26965  lmieu  27555  axlowdimlem14  27733  usgredg2v  28004  cusgrfilem3  28234  cusgrfi  28235  vtxdgoddnumeven  28330  clwwlknon1sn  28873  ex-natded5.13-2  29189  diffib  31276  ordtconnlem1  32309  eulerpartlemgh  32782  bnj23  33134  sleadd1im  34293  sleadd1  34295  nn0prpw  34727  meran1  34815  finxpreclem6  35799  wl-spae  35912  poimirlem32  36042  heiborlem1  36202  riotaclbgBAD  37348  aks6d1c2p2  40481  ioin9i8  40557  onsupmaxb  41476  onsupsucismax  41517  reclt0  43525  limclr  43791  eu2ndop1stv  45252  requad01  45708  mndpsuppss  46342  line2ylem  46732  line2xlem  46734
  Copyright terms: Public domain W3C validator